This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem exp11d

Description: exp11nnd for nonzero integer exponents. (Contributed by SN, 14-Sep-2023)

Ref Expression
Hypotheses exp11d.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
exp11d.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
exp11d.3 ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
exp11d.4 ⊢ ( 𝜑 → 𝑁 ≠ 0 )
exp11d.5 ⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) = ( 𝐵 ↑ 𝑁 ) )
Assertion exp11d ( 𝜑 → 𝐴 = 𝐵 )

Proof

Step Hyp Ref Expression
1 exp11d.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
2 exp11d.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
3 exp11d.3 ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
4 exp11d.4 ⊢ ( 𝜑 → 𝑁 ≠ 0 )
5 exp11d.5 ⊢ ( 𝜑 → ( 𝐴 ↑ 𝑁 ) = ( 𝐵 ↑ 𝑁 ) )
6 simpr ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → 𝑁 = 0 )
7 4 adantr ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → 𝑁 ≠ 0 )
8 6 7 pm2.21ddne ⊢ ( ( 𝜑 ∧ 𝑁 = 0 ) → 𝐴 = 𝐵 )
9 1 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → 𝐴 ∈ ℝ+ )
10 2 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → 𝐵 ∈ ℝ+ )
11 simpr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ )
12 5 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ↑ 𝑁 ) = ( 𝐵 ↑ 𝑁 ) )
13 9 10 11 12 exp11nnd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ℕ ) → 𝐴 = 𝐵 )
14 1 adantr ⊢ ( ( 𝜑 ∧ - 𝑁 ∈ ℕ ) → 𝐴 ∈ ℝ+ )
15 2 adantr ⊢ ( ( 𝜑 ∧ - 𝑁 ∈ ℕ ) → 𝐵 ∈ ℝ+ )
16 simpr ⊢ ( ( 𝜑 ∧ - 𝑁 ∈ ℕ ) → - 𝑁 ∈ ℕ )
17 14 rpcnd ⊢ ( ( 𝜑 ∧ - 𝑁 ∈ ℕ ) → 𝐴 ∈ ℂ )
18 16 nnnn0d ⊢ ( ( 𝜑 ∧ - 𝑁 ∈ ℕ ) → - 𝑁 ∈ ℕ0 )
19 17 18 expcld ⊢ ( ( 𝜑 ∧ - 𝑁 ∈ ℕ ) → ( 𝐴 ↑ - 𝑁 ) ∈ ℂ )
20 15 rpcnd ⊢ ( ( 𝜑 ∧ - 𝑁 ∈ ℕ ) → 𝐵 ∈ ℂ )
21 20 18 expcld ⊢ ( ( 𝜑 ∧ - 𝑁 ∈ ℕ ) → ( 𝐵 ↑ - 𝑁 ) ∈ ℂ )
22 14 rpne0d ⊢ ( ( 𝜑 ∧ - 𝑁 ∈ ℕ ) → 𝐴 ≠ 0 )
23 16 nnzd ⊢ ( ( 𝜑 ∧ - 𝑁 ∈ ℕ ) → - 𝑁 ∈ ℤ )
24 17 22 23 expne0d ⊢ ( ( 𝜑 ∧ - 𝑁 ∈ ℕ ) → ( 𝐴 ↑ - 𝑁 ) ≠ 0 )
25 15 rpne0d ⊢ ( ( 𝜑 ∧ - 𝑁 ∈ ℕ ) → 𝐵 ≠ 0 )
26 20 25 23 expne0d ⊢ ( ( 𝜑 ∧ - 𝑁 ∈ ℕ ) → ( 𝐵 ↑ - 𝑁 ) ≠ 0 )
27 5 adantr ⊢ ( ( 𝜑 ∧ - 𝑁 ∈ ℕ ) → ( 𝐴 ↑ 𝑁 ) = ( 𝐵 ↑ 𝑁 ) )
28 3 zcnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
29 28 adantr ⊢ ( ( 𝜑 ∧ - 𝑁 ∈ ℕ ) → 𝑁 ∈ ℂ )
30 expneg2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ - 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) = ( 1 / ( 𝐴 ↑ - 𝑁 ) ) )
31 17 29 18 30 syl3anc ⊢ ( ( 𝜑 ∧ - 𝑁 ∈ ℕ ) → ( 𝐴 ↑ 𝑁 ) = ( 1 / ( 𝐴 ↑ - 𝑁 ) ) )
32 expneg2 ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ - 𝑁 ∈ ℕ0 ) → ( 𝐵 ↑ 𝑁 ) = ( 1 / ( 𝐵 ↑ - 𝑁 ) ) )
33 20 29 18 32 syl3anc ⊢ ( ( 𝜑 ∧ - 𝑁 ∈ ℕ ) → ( 𝐵 ↑ 𝑁 ) = ( 1 / ( 𝐵 ↑ - 𝑁 ) ) )
34 27 31 33 3eqtr3d ⊢ ( ( 𝜑 ∧ - 𝑁 ∈ ℕ ) → ( 1 / ( 𝐴 ↑ - 𝑁 ) ) = ( 1 / ( 𝐵 ↑ - 𝑁 ) ) )
35 19 21 24 26 34 rec11d ⊢ ( ( 𝜑 ∧ - 𝑁 ∈ ℕ ) → ( 𝐴 ↑ - 𝑁 ) = ( 𝐵 ↑ - 𝑁 ) )
36 14 15 16 35 exp11nnd ⊢ ( ( 𝜑 ∧ - 𝑁 ∈ ℕ ) → 𝐴 = 𝐵 )
37 elz ⊢ ( 𝑁 ∈ ℤ ↔ ( 𝑁 ∈ ℝ ∧ ( 𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ ) ) )
38 3 37 sylib ⊢ ( 𝜑 → ( 𝑁 ∈ ℝ ∧ ( 𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ ) ) )
39 38 simprd ⊢ ( 𝜑 → ( 𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ - 𝑁 ∈ ℕ ) )
40 8 13 36 39 mpjao3dan ⊢ ( 𝜑 → 𝐴 = 𝐵 )