Metamath Proof Explorer

Theorem leexp2r

Description: Weak ordering relationship for exponentiation of a fixed real base in [ 0 , 1 ] to integer exponents. (Contributed by Paul Chapman, 14-Jan-2008) (Revised by Mario Carneiro, 29-Apr-2014)

Ref Expression
Assertion leexp2r 
|- ( ( ( A e. RR /\ M e. NN0 /\ N e. ( ZZ>= ` M ) ) /\ ( 0 <_ A /\ A <_ 1 ) ) -> ( A ^ N ) <_ ( A ^ M ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( j = M -> ( A ^ j ) = ( A ^ M ) )
2 1 breq1d 
 |-  ( j = M -> ( ( A ^ j ) <_ ( A ^ M ) <-> ( A ^ M ) <_ ( A ^ M ) ) )
3 2 imbi2d 
 |-  ( j = M -> ( ( ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) -> ( A ^ j ) <_ ( A ^ M ) ) <-> ( ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) -> ( A ^ M ) <_ ( A ^ M ) ) ) )
4 oveq2 
 |-  ( j = k -> ( A ^ j ) = ( A ^ k ) )
5 4 breq1d 
 |-  ( j = k -> ( ( A ^ j ) <_ ( A ^ M ) <-> ( A ^ k ) <_ ( A ^ M ) ) )
6 5 imbi2d 
 |-  ( j = k -> ( ( ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) -> ( A ^ j ) <_ ( A ^ M ) ) <-> ( ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) -> ( A ^ k ) <_ ( A ^ M ) ) ) )
7 oveq2 
 |-  ( j = ( k + 1 ) -> ( A ^ j ) = ( A ^ ( k + 1 ) ) )
8 7 breq1d 
 |-  ( j = ( k + 1 ) -> ( ( A ^ j ) <_ ( A ^ M ) <-> ( A ^ ( k + 1 ) ) <_ ( A ^ M ) ) )
9 8 imbi2d 
 |-  ( j = ( k + 1 ) -> ( ( ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) -> ( A ^ j ) <_ ( A ^ M ) ) <-> ( ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) -> ( A ^ ( k + 1 ) ) <_ ( A ^ M ) ) ) )
10 oveq2 
 |-  ( j = N -> ( A ^ j ) = ( A ^ N ) )
11 10 breq1d 
 |-  ( j = N -> ( ( A ^ j ) <_ ( A ^ M ) <-> ( A ^ N ) <_ ( A ^ M ) ) )
12 11 imbi2d 
 |-  ( j = N -> ( ( ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) -> ( A ^ j ) <_ ( A ^ M ) ) <-> ( ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) -> ( A ^ N ) <_ ( A ^ M ) ) ) )
13 reexpcl 
 |-  ( ( A e. RR /\ M e. NN0 ) -> ( A ^ M ) e. RR )
14 13 adantr 
 |-  ( ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) -> ( A ^ M ) e. RR )
15 14 leidd 
 |-  ( ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) -> ( A ^ M ) <_ ( A ^ M ) )
16 simprll 
 |-  ( ( k e. ( ZZ>= ` M ) /\ ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) ) -> A e. RR )
17 1red 
 |-  ( ( k e. ( ZZ>= ` M ) /\ ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) ) -> 1 e. RR )
18 simprlr 
 |-  ( ( k e. ( ZZ>= ` M ) /\ ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) ) -> M e. NN0 )
19 simpl 
 |-  ( ( k e. ( ZZ>= ` M ) /\ ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) ) -> k e. ( ZZ>= ` M ) )
20 eluznn0 
 |-  ( ( M e. NN0 /\ k e. ( ZZ>= ` M ) ) -> k e. NN0 )
21 18 19 20 syl2anc 
 |-  ( ( k e. ( ZZ>= ` M ) /\ ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) ) -> k e. NN0 )
22 reexpcl 
 |-  ( ( A e. RR /\ k e. NN0 ) -> ( A ^ k ) e. RR )
23 16 21 22 syl2anc 
 |-  ( ( k e. ( ZZ>= ` M ) /\ ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) ) -> ( A ^ k ) e. RR )
24 simprrl 
 |-  ( ( k e. ( ZZ>= ` M ) /\ ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) ) -> 0 <_ A )
25 expge0 
 |-  ( ( A e. RR /\ k e. NN0 /\ 0 <_ A ) -> 0 <_ ( A ^ k ) )
26 16 21 24 25 syl3anc 
 |-  ( ( k e. ( ZZ>= ` M ) /\ ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) ) -> 0 <_ ( A ^ k ) )
27 simprrr 
 |-  ( ( k e. ( ZZ>= ` M ) /\ ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) ) -> A <_ 1 )
28 16 17 23 26 27 lemul2ad 
 |-  ( ( k e. ( ZZ>= ` M ) /\ ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) ) -> ( ( A ^ k ) x. A ) <_ ( ( A ^ k ) x. 1 ) )
29 16 recnd 
 |-  ( ( k e. ( ZZ>= ` M ) /\ ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) ) -> A e. CC )
30 expp1 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( A ^ ( k + 1 ) ) = ( ( A ^ k ) x. A ) )
31 29 21 30 syl2anc 
 |-  ( ( k e. ( ZZ>= ` M ) /\ ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) ) -> ( A ^ ( k + 1 ) ) = ( ( A ^ k ) x. A ) )
32 23 recnd 
 |-  ( ( k e. ( ZZ>= ` M ) /\ ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) ) -> ( A ^ k ) e. CC )
33 32 mulridd 
 |-  ( ( k e. ( ZZ>= ` M ) /\ ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) ) -> ( ( A ^ k ) x. 1 ) = ( A ^ k ) )
34 33 eqcomd 
 |-  ( ( k e. ( ZZ>= ` M ) /\ ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) ) -> ( A ^ k ) = ( ( A ^ k ) x. 1 ) )
35 28 31 34 3brtr4d 
 |-  ( ( k e. ( ZZ>= ` M ) /\ ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) ) -> ( A ^ ( k + 1 ) ) <_ ( A ^ k ) )
36 peano2nn0 
 |-  ( k e. NN0 -> ( k + 1 ) e. NN0 )
37 21 36 syl 
 |-  ( ( k e. ( ZZ>= ` M ) /\ ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) ) -> ( k + 1 ) e. NN0 )
38 reexpcl 
 |-  ( ( A e. RR /\ ( k + 1 ) e. NN0 ) -> ( A ^ ( k + 1 ) ) e. RR )
39 16 37 38 syl2anc 
 |-  ( ( k e. ( ZZ>= ` M ) /\ ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) ) -> ( A ^ ( k + 1 ) ) e. RR )
40 13 ad2antrl 
 |-  ( ( k e. ( ZZ>= ` M ) /\ ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) ) -> ( A ^ M ) e. RR )
41 letr 
 |-  ( ( ( A ^ ( k + 1 ) ) e. RR /\ ( A ^ k ) e. RR /\ ( A ^ M ) e. RR ) -> ( ( ( A ^ ( k + 1 ) ) <_ ( A ^ k ) /\ ( A ^ k ) <_ ( A ^ M ) ) -> ( A ^ ( k + 1 ) ) <_ ( A ^ M ) ) )
42 39 23 40 41 syl3anc 
 |-  ( ( k e. ( ZZ>= ` M ) /\ ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) ) -> ( ( ( A ^ ( k + 1 ) ) <_ ( A ^ k ) /\ ( A ^ k ) <_ ( A ^ M ) ) -> ( A ^ ( k + 1 ) ) <_ ( A ^ M ) ) )
43 35 42 mpand 
 |-  ( ( k e. ( ZZ>= ` M ) /\ ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) ) -> ( ( A ^ k ) <_ ( A ^ M ) -> ( A ^ ( k + 1 ) ) <_ ( A ^ M ) ) )
44 43 ex 
 |-  ( k e. ( ZZ>= ` M ) -> ( ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) -> ( ( A ^ k ) <_ ( A ^ M ) -> ( A ^ ( k + 1 ) ) <_ ( A ^ M ) ) ) )
45 44 a2d 
 |-  ( k e. ( ZZ>= ` M ) -> ( ( ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) -> ( A ^ k ) <_ ( A ^ M ) ) -> ( ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) -> ( A ^ ( k + 1 ) ) <_ ( A ^ M ) ) ) )
46 3 6 9 12 15 45 uzind4i 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( ( A e. RR /\ M e. NN0 ) /\ ( 0 <_ A /\ A <_ 1 ) ) -> ( A ^ N ) <_ ( A ^ M ) ) )
47 46 expd 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( A e. RR /\ M e. NN0 ) -> ( ( 0 <_ A /\ A <_ 1 ) -> ( A ^ N ) <_ ( A ^ M ) ) ) )
48 47 com12 
 |-  ( ( A e. RR /\ M e. NN0 ) -> ( N e. ( ZZ>= ` M ) -> ( ( 0 <_ A /\ A <_ 1 ) -> ( A ^ N ) <_ ( A ^ M ) ) ) )
49 48 3impia 
 |-  ( ( A e. RR /\ M e. NN0 /\ N e. ( ZZ>= ` M ) ) -> ( ( 0 <_ A /\ A <_ 1 ) -> ( A ^ N ) <_ ( A ^ M ) ) )
50 49 imp 
 |-  ( ( ( A e. RR /\ M e. NN0 /\ N e. ( ZZ>= ` M ) ) /\ ( 0 <_ A /\ A <_ 1 ) ) -> ( A ^ N ) <_ ( A ^ M ) )