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

Metamath Proof Explorer

Theorem ltexp2a

Description: Exponent ordering relationship for exponentiation of a fixed real base greater than 1 to integer exponents. (Contributed by NM, 2-Aug-2006) (Revised by Mario Carneiro, 4-Jun-2014)

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

Proof

Step Hyp Ref Expression
1 simpl1 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ ( 1 < A /\ M < N ) ) -> A e. RR )
2 0red 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ ( 1 < A /\ M < N ) ) -> 0 e. RR )
3 1red 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ ( 1 < A /\ M < N ) ) -> 1 e. RR )
4 0lt1 
 |-  0 < 1
5 4 a1i 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ ( 1 < A /\ M < N ) ) -> 0 < 1 )
6 simprl 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ ( 1 < A /\ M < N ) ) -> 1 < A )
7 2 3 1 5 6 lttrd 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ ( 1 < A /\ M < N ) ) -> 0 < A )
8 1 7 elrpd 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ ( 1 < A /\ M < N ) ) -> A e. RR+ )
9 simpl2 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ ( 1 < A /\ M < N ) ) -> M e. ZZ )
10 rpexpcl 
 |-  ( ( A e. RR+ /\ M e. ZZ ) -> ( A ^ M ) e. RR+ )
11 8 9 10 syl2anc 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ ( 1 < A /\ M < N ) ) -> ( A ^ M ) e. RR+ )
12 11 rpred 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ ( 1 < A /\ M < N ) ) -> ( A ^ M ) e. RR )
13 12 recnd 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ ( 1 < A /\ M < N ) ) -> ( A ^ M ) e. CC )
14 13 mullidd 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ ( 1 < A /\ M < N ) ) -> ( 1 x. ( A ^ M ) ) = ( A ^ M ) )
15 simprr 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ ( 1 < A /\ M < N ) ) -> M < N )
16 simpl3 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ ( 1 < A /\ M < N ) ) -> N e. ZZ )
17 znnsub 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M < N <-> ( N - M ) e. NN ) )
18 9 16 17 syl2anc 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ ( 1 < A /\ M < N ) ) -> ( M < N <-> ( N - M ) e. NN ) )
19 15 18 mpbid 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ ( 1 < A /\ M < N ) ) -> ( N - M ) e. NN )
20 expgt1 
 |-  ( ( A e. RR /\ ( N - M ) e. NN /\ 1 < A ) -> 1 < ( A ^ ( N - M ) ) )
21 1 19 6 20 syl3anc 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ ( 1 < A /\ M < N ) ) -> 1 < ( A ^ ( N - M ) ) )
22 1 recnd 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ ( 1 < A /\ M < N ) ) -> A e. CC )
23 7 gt0ne0d 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ ( 1 < A /\ M < N ) ) -> A =/= 0 )
24 expsub 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( N e. ZZ /\ M e. ZZ ) ) -> ( A ^ ( N - M ) ) = ( ( A ^ N ) / ( A ^ M ) ) )
25 22 23 16 9 24 syl22anc 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ ( 1 < A /\ M < N ) ) -> ( A ^ ( N - M ) ) = ( ( A ^ N ) / ( A ^ M ) ) )
26 21 25 breqtrd 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ ( 1 < A /\ M < N ) ) -> 1 < ( ( A ^ N ) / ( A ^ M ) ) )
27 rpexpcl 
 |-  ( ( A e. RR+ /\ N e. ZZ ) -> ( A ^ N ) e. RR+ )
28 8 16 27 syl2anc 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ ( 1 < A /\ M < N ) ) -> ( A ^ N ) e. RR+ )
29 28 rpred 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ ( 1 < A /\ M < N ) ) -> ( A ^ N ) e. RR )
30 3 29 11 ltmuldivd 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ ( 1 < A /\ M < N ) ) -> ( ( 1 x. ( A ^ M ) ) < ( A ^ N ) <-> 1 < ( ( A ^ N ) / ( A ^ M ) ) ) )
31 26 30 mpbird 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ ( 1 < A /\ M < N ) ) -> ( 1 x. ( A ^ M ) ) < ( A ^ N ) )
32 14 31 eqbrtrrd 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ ( 1 < A /\ M < N ) ) -> ( A ^ M ) < ( A ^ N ) )