Metamath Proof Explorer

Theorem leexp2

Description: Ordering law for exponentiation of a fixed real base greater than 1 to integer exponents. (Contributed by Mario Carneiro, 26-Apr-2016)

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

Proof

Step Hyp Ref Expression
1 3ancomb 
 |-  ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) <-> ( A e. RR /\ N e. ZZ /\ M e. ZZ ) )
2 ltexp2 
 |-  ( ( ( A e. RR /\ N e. ZZ /\ M e. ZZ ) /\ 1 < A ) -> ( N < M <-> ( A ^ N ) < ( A ^ M ) ) )
3 1 2 sylanb 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ 1 < A ) -> ( N < M <-> ( A ^ N ) < ( A ^ M ) ) )
4 3 notbid 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ 1 < A ) -> ( -. N < M <-> -. ( A ^ N ) < ( A ^ M ) ) )
5 simpl2 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ 1 < A ) -> M e. ZZ )
6 simpl3 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ 1 < A ) -> N e. ZZ )
7 zre 
 |-  ( M e. ZZ -> M e. RR )
8 zre 
 |-  ( N e. ZZ -> N e. RR )
9 lenlt 
 |-  ( ( M e. RR /\ N e. RR ) -> ( M <_ N <-> -. N < M ) )
10 7 8 9 syl2an 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M <_ N <-> -. N < M ) )
11 5 6 10 syl2anc 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ 1 < A ) -> ( M <_ N <-> -. N < M ) )
12 simpl1 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ 1 < A ) -> A e. RR )
13 0red 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ 1 < A ) -> 0 e. RR )
14 1red 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ 1 < A ) -> 1 e. RR )
15 0lt1 
 |-  0 < 1
16 15 a1i 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ 1 < A ) -> 0 < 1 )
17 simpr 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ 1 < A ) -> 1 < A )
18 13 14 12 16 17 lttrd 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ 1 < A ) -> 0 < A )
19 18 gt0ne0d 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ 1 < A ) -> A =/= 0 )
20 reexpclz 
 |-  ( ( A e. RR /\ A =/= 0 /\ M e. ZZ ) -> ( A ^ M ) e. RR )
21 12 19 5 20 syl3anc 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ 1 < A ) -> ( A ^ M ) e. RR )
22 reexpclz 
 |-  ( ( A e. RR /\ A =/= 0 /\ N e. ZZ ) -> ( A ^ N ) e. RR )
23 12 19 6 22 syl3anc 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ 1 < A ) -> ( A ^ N ) e. RR )
24 21 23 lenltd 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ 1 < A ) -> ( ( A ^ M ) <_ ( A ^ N ) <-> -. ( A ^ N ) < ( A ^ M ) ) )
25 4 11 24 3bitr4d 
 |-  ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ 1 < A ) -> ( M <_ N <-> ( A ^ M ) <_ ( A ^ N ) ) )