Metamath Proof Explorer

Theorem expneg

Description: Value of a complex number raised to a negative integer power. (Contributed by Mario Carneiro, 4-Jun-2014)

Ref Expression
Assertion expneg ⊢ A ∈ ℂ ∧ N ∈ ℕ 0 → A − N = 1 A N

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ N ∈ ℕ 0 ↔ N ∈ ℕ ∨ N = 0
2 nnne0 ⊢ N ∈ ℕ → N ≠ 0
3 2 adantl ⊢ A ∈ ℂ ∧ N ∈ ℕ → N ≠ 0
4 nncn ⊢ N ∈ ℕ → N ∈ ℂ
5 4 adantl ⊢ A ∈ ℂ ∧ N ∈ ℕ → N ∈ ℂ
6 5 negeq0d ⊢ A ∈ ℂ ∧ N ∈ ℕ → N = 0 ↔ − N = 0
7 6 necon3abid ⊢ A ∈ ℂ ∧ N ∈ ℕ → N ≠ 0 ↔ ¬ − N = 0
8 3 7 mpbid ⊢ A ∈ ℂ ∧ N ∈ ℕ → ¬ − N = 0
9 8 iffalsed ⊢ A ∈ ℂ ∧ N ∈ ℕ → if − N = 0 1 if 0 < − N seq 1 × ℕ × A ⁡ − N 1 seq 1 × ℕ × A ⁡ − -N = if 0 < − N seq 1 × ℕ × A ⁡ − N 1 seq 1 × ℕ × A ⁡ − -N
10 nnnn0 ⊢ N ∈ ℕ → N ∈ ℕ 0
11 10 adantl ⊢ A ∈ ℂ ∧ N ∈ ℕ → N ∈ ℕ 0
12 nn0nlt0 ⊢ N ∈ ℕ 0 → ¬ N < 0
13 11 12 syl ⊢ A ∈ ℂ ∧ N ∈ ℕ → ¬ N < 0
14 11 nn0red ⊢ A ∈ ℂ ∧ N ∈ ℕ → N ∈ ℝ
15 14 lt0neg1d ⊢ A ∈ ℂ ∧ N ∈ ℕ → N < 0 ↔ 0 < − N
16 13 15 mtbid ⊢ A ∈ ℂ ∧ N ∈ ℕ → ¬ 0 < − N
17 16 iffalsed ⊢ A ∈ ℂ ∧ N ∈ ℕ → if 0 < − N seq 1 × ℕ × A ⁡ − N 1 seq 1 × ℕ × A ⁡ − -N = 1 seq 1 × ℕ × A ⁡ − -N
18 5 negnegd ⊢ A ∈ ℂ ∧ N ∈ ℕ → − -N = N
19 18 fveq2d ⊢ A ∈ ℂ ∧ N ∈ ℕ → seq 1 × ℕ × A ⁡ − -N = seq 1 × ℕ × A ⁡ N
20 19 oveq2d ⊢ A ∈ ℂ ∧ N ∈ ℕ → 1 seq 1 × ℕ × A ⁡ − -N = 1 seq 1 × ℕ × A ⁡ N
21 9 17 20 3eqtrd ⊢ A ∈ ℂ ∧ N ∈ ℕ → if − N = 0 1 if 0 < − N seq 1 × ℕ × A ⁡ − N 1 seq 1 × ℕ × A ⁡ − -N = 1 seq 1 × ℕ × A ⁡ N
22 nnnegz ⊢ N ∈ ℕ → − N ∈ ℤ
23 expval ⊢ A ∈ ℂ ∧ − N ∈ ℤ → A − N = if − N = 0 1 if 0 < − N seq 1 × ℕ × A ⁡ − N 1 seq 1 × ℕ × A ⁡ − -N
24 22 23 sylan2 ⊢ A ∈ ℂ ∧ N ∈ ℕ → A − N = if − N = 0 1 if 0 < − N seq 1 × ℕ × A ⁡ − N 1 seq 1 × ℕ × A ⁡ − -N
25 expnnval ⊢ A ∈ ℂ ∧ N ∈ ℕ → A N = seq 1 × ℕ × A ⁡ N
26 25 oveq2d ⊢ A ∈ ℂ ∧ N ∈ ℕ → 1 A N = 1 seq 1 × ℕ × A ⁡ N
27 21 24 26 3eqtr4d ⊢ A ∈ ℂ ∧ N ∈ ℕ → A − N = 1 A N
28 1div1e1 ⊢ 1 1 = 1
29 28 eqcomi ⊢ 1 = 1 1
30 negeq ⊢ N = 0 → − N = − 0
31 neg0 ⊢ − 0 = 0
32 30 31 eqtrdi ⊢ N = 0 → − N = 0
33 32 oveq2d ⊢ N = 0 → A − N = A 0
34 exp0 ⊢ A ∈ ℂ → A 0 = 1
35 33 34 sylan9eqr ⊢ A ∈ ℂ ∧ N = 0 → A − N = 1
36 oveq2 ⊢ N = 0 → A N = A 0
37 36 34 sylan9eqr ⊢ A ∈ ℂ ∧ N = 0 → A N = 1
38 37 oveq2d ⊢ A ∈ ℂ ∧ N = 0 → 1 A N = 1 1
39 29 35 38 3eqtr4a ⊢ A ∈ ℂ ∧ N = 0 → A − N = 1 A N
40 27 39 jaodan ⊢ A ∈ ℂ ∧ N ∈ ℕ ∨ N = 0 → A − N = 1 A N
41 1 40 sylan2b ⊢ A ∈ ℂ ∧ N ∈ ℕ 0 → A − N = 1 A N