Metamath Proof Explorer


Theorem leexp2r

Description: Weak ordering relationship for exponentiation. (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 mulid1d
 |-  ( ( 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 ) )