Step |
Hyp |
Ref |
Expression |
1 |
|
oveq2 |
|- ( x = y -> ( A ^ x ) = ( A ^ y ) ) |
2 |
|
oveq2 |
|- ( x = M -> ( A ^ x ) = ( A ^ M ) ) |
3 |
|
oveq2 |
|- ( x = N -> ( A ^ x ) = ( A ^ N ) ) |
4 |
|
zssre |
|- ZZ C_ RR |
5 |
|
simpl |
|- ( ( A e. RR /\ 1 < A ) -> A e. RR ) |
6 |
|
0red |
|- ( ( A e. RR /\ 1 < A ) -> 0 e. RR ) |
7 |
|
1red |
|- ( ( A e. RR /\ 1 < A ) -> 1 e. RR ) |
8 |
|
0lt1 |
|- 0 < 1 |
9 |
8
|
a1i |
|- ( ( A e. RR /\ 1 < A ) -> 0 < 1 ) |
10 |
|
simpr |
|- ( ( A e. RR /\ 1 < A ) -> 1 < A ) |
11 |
6 7 5 9 10
|
lttrd |
|- ( ( A e. RR /\ 1 < A ) -> 0 < A ) |
12 |
5 11
|
elrpd |
|- ( ( A e. RR /\ 1 < A ) -> A e. RR+ ) |
13 |
|
rpexpcl |
|- ( ( A e. RR+ /\ x e. ZZ ) -> ( A ^ x ) e. RR+ ) |
14 |
12 13
|
sylan |
|- ( ( ( A e. RR /\ 1 < A ) /\ x e. ZZ ) -> ( A ^ x ) e. RR+ ) |
15 |
14
|
rpred |
|- ( ( ( A e. RR /\ 1 < A ) /\ x e. ZZ ) -> ( A ^ x ) e. RR ) |
16 |
|
simpll |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> A e. RR ) |
17 |
|
simprl |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> x e. ZZ ) |
18 |
|
simprr |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> y e. ZZ ) |
19 |
|
simplr |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> 1 < A ) |
20 |
|
ltexp2a |
|- ( ( ( A e. RR /\ x e. ZZ /\ y e. ZZ ) /\ ( 1 < A /\ x < y ) ) -> ( A ^ x ) < ( A ^ y ) ) |
21 |
20
|
expr |
|- ( ( ( A e. RR /\ x e. ZZ /\ y e. ZZ ) /\ 1 < A ) -> ( x < y -> ( A ^ x ) < ( A ^ y ) ) ) |
22 |
16 17 18 19 21
|
syl31anc |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( x < y -> ( A ^ x ) < ( A ^ y ) ) ) |
23 |
1 2 3 4 15 22
|
eqord1 |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( M = N <-> ( A ^ M ) = ( A ^ N ) ) ) |
24 |
23
|
ancom2s |
|- ( ( ( A e. RR /\ 1 < A ) /\ ( N e. ZZ /\ M e. ZZ ) ) -> ( M = N <-> ( A ^ M ) = ( A ^ N ) ) ) |
25 |
24
|
exp43 |
|- ( A e. RR -> ( 1 < A -> ( N e. ZZ -> ( M e. ZZ -> ( M = N <-> ( A ^ M ) = ( A ^ N ) ) ) ) ) ) |
26 |
25
|
com24 |
|- ( A e. RR -> ( M e. ZZ -> ( N e. ZZ -> ( 1 < A -> ( M = N <-> ( A ^ M ) = ( A ^ N ) ) ) ) ) ) |
27 |
26
|
3imp1 |
|- ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ 1 < A ) -> ( M = N <-> ( A ^ M ) = ( A ^ N ) ) ) |
28 |
27
|
bicomd |
|- ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ 1 < A ) -> ( ( A ^ M ) = ( A ^ N ) <-> M = N ) ) |