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 ⊢ φ → A N = B N
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 ⊢ φ → A N = B N
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 ∈ ℕ → A N = B N
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 ∈ ℕ → A N = B N
28 3 zcnd ⊢ φ → N ∈ ℂ
29 28 adantr ⊢ φ ∧ − N ∈ ℕ → N ∈ ℂ
30 expneg2 ⊢ A ∈ ℂ ∧ N ∈ ℂ ∧ − N ∈ ℕ 0 → A N = 1 A − N
31 17 29 18 30 syl3anc ⊢ φ ∧ − N ∈ ℕ → A N = 1 A − N
32 expneg2 ⊢ B ∈ ℂ ∧ N ∈ ℂ ∧ − N ∈ ℕ 0 → B N = 1 B − N
33 20 29 18 32 syl3anc ⊢ φ ∧ − N ∈ ℕ → B N = 1 B − N
34 27 31 33 3eqtr3d ⊢ φ ∧ − N ∈ ℕ → 1 A − N = 1 B − 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