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 M N 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
5 simpl A 1 < A A
6 0red A 1 < A 0
7 1red A 1 < A 1
8 0lt1 0 < 1
9 8 a1i A 1 < A 0 < 1
10 simpr A 1 < A 1 < A
11 6 7 5 9 10 lttrd A 1 < A 0 < A
12 5 11 elrpd A 1 < A A +
13 rpexpcl A + x A x +
14 12 13 sylan A 1 < A x A x +
15 14 rpred A 1 < A x A x
16 simpll A 1 < A x y A
17 simprl A 1 < A x y x
18 simprr A 1 < A x y y
19 simplr A 1 < A x y 1 < A
20 ltexp2a A x y 1 < A x < y A x < A y
21 20 expr A x y 1 < A x < y A x < A y
22 16 17 18 19 21 syl31anc A 1 < A x y x < y A x < A y
23 1 2 3 4 15 22 eqord1 A 1 < A M N M = N A M = A N
24 23 ancom2s A 1 < A N M M = N A M = A N
25 24 exp43 A 1 < A N M M = N A M = A N
26 25 com24 A M N 1 < A M = N A M = A N
27 26 3imp1 A M N 1 < A M = N A M = A N
28 27 bicomd A M N 1 < A A M = A N M = N