Metamath Proof Explorer

Theorem expcan

Description: Cancellation law for exponentiation. (Contributed by NM, 2-Aug-2006) (Revised by Mario Carneiro, 4-Jun-2014)

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

Proof

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