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 ) ) ) |