Proof of Theorem expneg
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elnn0 12528 | . 2
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℕ
∨ 𝑁 =
0)) | 
| 2 |  | nnne0 12300 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) | 
| 3 | 2 | adantl 481 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → 𝑁 ≠ 0) | 
| 4 |  | nncn 12274 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) | 
| 5 | 4 | adantl 481 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℂ) | 
| 6 | 5 | negeq0d 11612 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝑁 = 0 ↔ -𝑁 = 0)) | 
| 7 | 6 | necon3abid 2977 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝑁 ≠ 0 ↔ ¬ -𝑁 = 0)) | 
| 8 | 3, 7 | mpbid 232 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ¬
-𝑁 = 0) | 
| 9 | 8 | iffalsed 4536 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) →
if(-𝑁 = 0, 1, if(0 <
-𝑁, (seq1( · ,
(ℕ × {𝐴}))‘-𝑁), (1 / (seq1( · , (ℕ ×
{𝐴}))‘--𝑁)))) = if(0 < -𝑁, (seq1( · , (ℕ
× {𝐴}))‘-𝑁), (1 / (seq1( · ,
(ℕ × {𝐴}))‘--𝑁)))) | 
| 10 |  | nnnn0 12533 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) | 
| 11 | 10 | adantl 481 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℕ0) | 
| 12 |  | nn0nlt0 12552 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ ¬ 𝑁 <
0) | 
| 13 | 11, 12 | syl 17 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ¬
𝑁 < 0) | 
| 14 | 11 | nn0red 12588 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℝ) | 
| 15 | 14 | lt0neg1d 11832 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝑁 < 0 ↔ 0 < -𝑁)) | 
| 16 | 13, 15 | mtbid 324 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ¬ 0
< -𝑁) | 
| 17 | 16 | iffalsed 4536 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → if(0
< -𝑁, (seq1( · ,
(ℕ × {𝐴}))‘-𝑁), (1 / (seq1( · , (ℕ ×
{𝐴}))‘--𝑁))) = (1 / (seq1( · ,
(ℕ × {𝐴}))‘--𝑁))) | 
| 18 | 5 | negnegd 11611 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → --𝑁 = 𝑁) | 
| 19 | 18 | fveq2d 6910 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (seq1(
· , (ℕ × {𝐴}))‘--𝑁) = (seq1( · , (ℕ ×
{𝐴}))‘𝑁)) | 
| 20 | 19 | oveq2d 7447 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (1 /
(seq1( · , (ℕ × {𝐴}))‘--𝑁)) = (1 / (seq1( · , (ℕ ×
{𝐴}))‘𝑁))) | 
| 21 | 9, 17, 20 | 3eqtrd 2781 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) →
if(-𝑁 = 0, 1, if(0 <
-𝑁, (seq1( · ,
(ℕ × {𝐴}))‘-𝑁), (1 / (seq1( · , (ℕ ×
{𝐴}))‘--𝑁)))) = (1 / (seq1( · ,
(ℕ × {𝐴}))‘𝑁))) | 
| 22 |  | nnnegz 12616 | . . . . 5
⊢ (𝑁 ∈ ℕ → -𝑁 ∈
ℤ) | 
| 23 |  | expval 14104 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ -𝑁 ∈ ℤ) → (𝐴↑-𝑁) = if(-𝑁 = 0, 1, if(0 < -𝑁, (seq1( · , (ℕ × {𝐴}))‘-𝑁), (1 / (seq1( · , (ℕ ×
{𝐴}))‘--𝑁))))) | 
| 24 | 22, 23 | sylan2 593 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝐴↑-𝑁) = if(-𝑁 = 0, 1, if(0 < -𝑁, (seq1( · , (ℕ × {𝐴}))‘-𝑁), (1 / (seq1( · , (ℕ ×
{𝐴}))‘--𝑁))))) | 
| 25 |  | expnnval 14105 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝐴↑𝑁) = (seq1( · , (ℕ ×
{𝐴}))‘𝑁)) | 
| 26 | 25 | oveq2d 7447 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (1 /
(𝐴↑𝑁)) = (1 / (seq1( · , (ℕ ×
{𝐴}))‘𝑁))) | 
| 27 | 21, 24, 26 | 3eqtr4d 2787 | . . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ) → (𝐴↑-𝑁) = (1 / (𝐴↑𝑁))) | 
| 28 |  | 1div1e1 11958 | . . . . 5
⊢ (1 / 1) =
1 | 
| 29 | 28 | eqcomi 2746 | . . . 4
⊢ 1 = (1 /
1) | 
| 30 |  | negeq 11500 | . . . . . . 7
⊢ (𝑁 = 0 → -𝑁 = -0) | 
| 31 |  | neg0 11555 | . . . . . . 7
⊢ -0 =
0 | 
| 32 | 30, 31 | eqtrdi 2793 | . . . . . 6
⊢ (𝑁 = 0 → -𝑁 = 0) | 
| 33 | 32 | oveq2d 7447 | . . . . 5
⊢ (𝑁 = 0 → (𝐴↑-𝑁) = (𝐴↑0)) | 
| 34 |  | exp0 14106 | . . . . 5
⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1) | 
| 35 | 33, 34 | sylan9eqr 2799 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 = 0) → (𝐴↑-𝑁) = 1) | 
| 36 |  | oveq2 7439 | . . . . . 6
⊢ (𝑁 = 0 → (𝐴↑𝑁) = (𝐴↑0)) | 
| 37 | 36, 34 | sylan9eqr 2799 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 = 0) → (𝐴↑𝑁) = 1) | 
| 38 | 37 | oveq2d 7447 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 = 0) → (1 / (𝐴↑𝑁)) = (1 / 1)) | 
| 39 | 29, 35, 38 | 3eqtr4a 2803 | . . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 = 0) → (𝐴↑-𝑁) = (1 / (𝐴↑𝑁))) | 
| 40 | 27, 39 | jaodan 960 | . 2
⊢ ((𝐴 ∈ ℂ ∧ (𝑁 ∈ ℕ ∨ 𝑁 = 0)) → (𝐴↑-𝑁) = (1 / (𝐴↑𝑁))) | 
| 41 | 1, 40 | sylan2b 594 | 1
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (𝐴↑-𝑁) = (1 / (𝐴↑𝑁))) |