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 ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → ( ( 𝐴𝑀 ) = ( 𝐴𝑁 ) ↔ 𝑀 = 𝑁 ) )

Proof

Step Hyp Ref Expression
1 oveq2 ( 𝑥 = 𝑦 → ( 𝐴𝑥 ) = ( 𝐴𝑦 ) )
2 oveq2 ( 𝑥 = 𝑀 → ( 𝐴𝑥 ) = ( 𝐴𝑀 ) )
3 oveq2 ( 𝑥 = 𝑁 → ( 𝐴𝑥 ) = ( 𝐴𝑁 ) )
4 zssre ℤ ⊆ ℝ
5 simpl ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 𝐴 ∈ ℝ )
6 0red ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 0 ∈ ℝ )
7 1red ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 1 ∈ ℝ )
8 0lt1 0 < 1
9 8 a1i ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 0 < 1 )
10 simpr ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 1 < 𝐴 )
11 6 7 5 9 10 lttrd ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 0 < 𝐴 )
12 5 11 elrpd ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 𝐴 ∈ ℝ+ )
13 rpexpcl ( ( 𝐴 ∈ ℝ+𝑥 ∈ ℤ ) → ( 𝐴𝑥 ) ∈ ℝ+ )
14 12 13 sylan ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑥 ∈ ℤ ) → ( 𝐴𝑥 ) ∈ ℝ+ )
15 14 rpred ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑥 ∈ ℤ ) → ( 𝐴𝑥 ) ∈ ℝ )
16 simpll ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝐴 ∈ ℝ )
17 simprl ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝑥 ∈ ℤ )
18 simprr ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝑦 ∈ ℤ )
19 simplr ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 1 < 𝐴 )
20 ltexp2a ( ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 1 < 𝐴𝑥 < 𝑦 ) ) → ( 𝐴𝑥 ) < ( 𝐴𝑦 ) )
21 20 expr ( ( ( 𝐴 ∈ ℝ ∧ 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ 1 < 𝐴 ) → ( 𝑥 < 𝑦 → ( 𝐴𝑥 ) < ( 𝐴𝑦 ) ) )
22 16 17 18 19 21 syl31anc ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝑥 < 𝑦 → ( 𝐴𝑥 ) < ( 𝐴𝑦 ) ) )
23 1 2 3 4 15 22 eqord1 ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑀 = 𝑁 ↔ ( 𝐴𝑀 ) = ( 𝐴𝑁 ) ) )
24 23 ancom2s ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ) → ( 𝑀 = 𝑁 ↔ ( 𝐴𝑀 ) = ( 𝐴𝑁 ) ) )
25 24 exp43 ( 𝐴 ∈ ℝ → ( 1 < 𝐴 → ( 𝑁 ∈ ℤ → ( 𝑀 ∈ ℤ → ( 𝑀 = 𝑁 ↔ ( 𝐴𝑀 ) = ( 𝐴𝑁 ) ) ) ) ) )
26 25 com24 ( 𝐴 ∈ ℝ → ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ℤ → ( 1 < 𝐴 → ( 𝑀 = 𝑁 ↔ ( 𝐴𝑀 ) = ( 𝐴𝑁 ) ) ) ) ) )
27 26 3imp1 ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → ( 𝑀 = 𝑁 ↔ ( 𝐴𝑀 ) = ( 𝐴𝑁 ) ) )
28 27 bicomd ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 1 < 𝐴 ) → ( ( 𝐴𝑀 ) = ( 𝐴𝑁 ) ↔ 𝑀 = 𝑁 ) )