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