Metamath Proof Explorer

Theorem leexp2a

Description: Weak ordering relationship for exponentiation of a fixed real base greater than or equal to 1 to integer exponents. (Contributed by NM, 14-Dec-2005) (Revised by Mario Carneiro, 5-Jun-2014)

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

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. RR /\ 1 <_ A /\ N e. ( ZZ>= ` M ) ) -> A e. RR )
2 0red 
 |-  ( ( A e. RR /\ 1 <_ A /\ N e. ( ZZ>= ` M ) ) -> 0 e. RR )
3 1red 
 |-  ( ( A e. RR /\ 1 <_ A /\ N e. ( ZZ>= ` M ) ) -> 1 e. RR )
4 0lt1 
 |-  0 < 1
5 4 a1i 
 |-  ( ( A e. RR /\ 1 <_ A /\ N e. ( ZZ>= ` M ) ) -> 0 < 1 )
6 simp2 
 |-  ( ( A e. RR /\ 1 <_ A /\ N e. ( ZZ>= ` M ) ) -> 1 <_ A )
7 2 3 1 5 6 ltletrd 
 |-  ( ( A e. RR /\ 1 <_ A /\ N e. ( ZZ>= ` M ) ) -> 0 < A )
8 1 7 elrpd 
 |-  ( ( A e. RR /\ 1 <_ A /\ N e. ( ZZ>= ` M ) ) -> A e. RR+ )
9 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
10 9 3ad2ant3 
 |-  ( ( A e. RR /\ 1 <_ A /\ N e. ( ZZ>= ` M ) ) -> M e. ZZ )
11 rpexpcl 
 |-  ( ( A e. RR+ /\ M e. ZZ ) -> ( A ^ M ) e. RR+ )
12 8 10 11 syl2anc 
 |-  ( ( A e. RR /\ 1 <_ A /\ N e. ( ZZ>= ` M ) ) -> ( A ^ M ) e. RR+ )
13 12 rpred 
 |-  ( ( A e. RR /\ 1 <_ A /\ N e. ( ZZ>= ` M ) ) -> ( A ^ M ) e. RR )
14 13 recnd 
 |-  ( ( A e. RR /\ 1 <_ A /\ N e. ( ZZ>= ` M ) ) -> ( A ^ M ) e. CC )
15 14 mullidd 
 |-  ( ( A e. RR /\ 1 <_ A /\ N e. ( ZZ>= ` M ) ) -> ( 1 x. ( A ^ M ) ) = ( A ^ M ) )
16 uznn0sub 
 |-  ( N e. ( ZZ>= ` M ) -> ( N - M ) e. NN0 )
17 16 3ad2ant3 
 |-  ( ( A e. RR /\ 1 <_ A /\ N e. ( ZZ>= ` M ) ) -> ( N - M ) e. NN0 )
18 expge1 
 |-  ( ( A e. RR /\ ( N - M ) e. NN0 /\ 1 <_ A ) -> 1 <_ ( A ^ ( N - M ) ) )
19 1 17 6 18 syl3anc 
 |-  ( ( A e. RR /\ 1 <_ A /\ N e. ( ZZ>= ` M ) ) -> 1 <_ ( A ^ ( N - M ) ) )
20 1 recnd 
 |-  ( ( A e. RR /\ 1 <_ A /\ N e. ( ZZ>= ` M ) ) -> A e. CC )
21 7 gt0ne0d 
 |-  ( ( A e. RR /\ 1 <_ A /\ N e. ( ZZ>= ` M ) ) -> A =/= 0 )
22 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
23 22 3ad2ant3 
 |-  ( ( A e. RR /\ 1 <_ A /\ N e. ( ZZ>= ` M ) ) -> N e. ZZ )
24 expsub 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. ZZ /\ M e. ZZ ) ) -> ( A ^ ( N - M ) ) = ( ( A ^ N ) / ( A ^ M ) ) )
25 20 21 23 10 24 syl22anc 
 |-  ( ( A e. RR /\ 1 <_ A /\ N e. ( ZZ>= ` M ) ) -> ( A ^ ( N - M ) ) = ( ( A ^ N ) / ( A ^ M ) ) )
26 19 25 breqtrd 
 |-  ( ( A e. RR /\ 1 <_ A /\ N e. ( ZZ>= ` M ) ) -> 1 <_ ( ( A ^ N ) / ( A ^ M ) ) )
27 rpexpcl 
 |-  ( ( A e. RR+ /\ N e. ZZ ) -> ( A ^ N ) e. RR+ )
28 8 23 27 syl2anc 
 |-  ( ( A e. RR /\ 1 <_ A /\ N e. ( ZZ>= ` M ) ) -> ( A ^ N ) e. RR+ )
29 28 rpred 
 |-  ( ( A e. RR /\ 1 <_ A /\ N e. ( ZZ>= ` M ) ) -> ( A ^ N ) e. RR )
30 3 29 12 lemuldivd 
 |-  ( ( A e. RR /\ 1 <_ A /\ N e. ( ZZ>= ` M ) ) -> ( ( 1 x. ( A ^ M ) ) <_ ( A ^ N ) <-> 1 <_ ( ( A ^ N ) / ( A ^ M ) ) ) )
31 26 30 mpbird 
 |-  ( ( A e. RR /\ 1 <_ A /\ N e. ( ZZ>= ` M ) ) -> ( 1 x. ( A ^ M ) ) <_ ( A ^ N ) )
32 15 31 eqbrtrrd 
 |-  ( ( A e. RR /\ 1 <_ A /\ N e. ( ZZ>= ` M ) ) -> ( A ^ M ) <_ ( A ^ N ) )