Metamath Proof Explorer

Theorem exp11d

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

Ref Expression
Hypotheses exp11d.1 ⊢φ→A∈ℝ+
exp11d.2 ⊢φ→B∈ℝ+
exp11d.3 ⊢φ→N∈ℤ
exp11d.4 ⊢φ→N≠0
exp11d.5 ⊢φ→AN=BN
Assertion exp11d ⊢φ→A=B

Proof

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