This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem explt1d

Description: A nonnegative real number less than one raised to a positive integer is less than one. (Contributed by SN, 3-Jul-2025)

Ref Expression
Hypotheses explt1d.a 
|- ( ph -> A e. RR )
explt1d.n 
|- ( ph -> N e. NN )
explt1d.0 
|- ( ph -> 0 <_ A )
explt1d.1 
|- ( ph -> A < 1 )
Assertion explt1d 
|- ( ph -> ( A ^ N ) < 1 )

Proof

Step Hyp Ref Expression
1 explt1d.a 
 |-  ( ph -> A e. RR )
2 explt1d.n 
 |-  ( ph -> N e. NN )
3 explt1d.0 
 |-  ( ph -> 0 <_ A )
4 explt1d.1 
 |-  ( ph -> A < 1 )
5 oveq1 
 |-  ( A = 0 -> ( A ^ N ) = ( 0 ^ N ) )
6 5 breq1d 
 |-  ( A = 0 -> ( ( A ^ N ) < ( 1 ^ N ) <-> ( 0 ^ N ) < ( 1 ^ N ) ) )
7 1 adantr 
 |-  ( ( ph /\ A =/= 0 ) -> A e. RR )
8 3 adantr 
 |-  ( ( ph /\ A =/= 0 ) -> 0 <_ A )
9 simpr 
 |-  ( ( ph /\ A =/= 0 ) -> A =/= 0 )
10 7 8 9 ne0gt0d 
 |-  ( ( ph /\ A =/= 0 ) -> 0 < A )
11 7 10 elrpd 
 |-  ( ( ph /\ A =/= 0 ) -> A e. RR+ )
12 simpr 
 |-  ( ( ph /\ A e. RR+ ) -> A e. RR+ )
13 1rp 
 |-  1 e. RR+
14 13 a1i 
 |-  ( ( ph /\ A e. RR+ ) -> 1 e. RR+ )
15 2 adantr 
 |-  ( ( ph /\ A e. RR+ ) -> N e. NN )
16 4 adantr 
 |-  ( ( ph /\ A e. RR+ ) -> A < 1 )
17 12 14 15 16 ltexp1dd 
 |-  ( ( ph /\ A e. RR+ ) -> ( A ^ N ) < ( 1 ^ N ) )
18 11 17 syldan 
 |-  ( ( ph /\ A =/= 0 ) -> ( A ^ N ) < ( 1 ^ N ) )
19 0lt1 
 |-  0 < 1
20 19 a1i 
 |-  ( ph -> 0 < 1 )
21 2 0expd 
 |-  ( ph -> ( 0 ^ N ) = 0 )
22 2 nnzd 
 |-  ( ph -> N e. ZZ )
23 1exp 
 |-  ( N e. ZZ -> ( 1 ^ N ) = 1 )
24 22 23 syl 
 |-  ( ph -> ( 1 ^ N ) = 1 )
25 20 21 24 3brtr4d 
 |-  ( ph -> ( 0 ^ N ) < ( 1 ^ N ) )
26 6 18 25 pm2.61ne 
 |-  ( ph -> ( A ^ N ) < ( 1 ^ N ) )
27 26 24 breqtrd 
 |-  ( ph -> ( A ^ N ) < 1 )