Metamath Proof Explorer


Theorem leexp2

Description: Ordering law for exponentiation. (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 ) ) )