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 < 𝐴 ) → ( ( 𝐴 ↑ 𝑀 ) = ( 𝐴 ↑ 𝑁 ) ↔ 𝑀 = 𝑁 ) )