| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | zcn 12618 | . . . 4
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) | 
| 2 |  | mulcom 11241 | . . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝐴 · 𝑁) = (𝑁 · 𝐴)) | 
| 3 | 1, 2 | sylan2 593 | . . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) → (𝐴 · 𝑁) = (𝑁 · 𝐴)) | 
| 4 | 3 | fveq2d 6910 | . 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) →
(exp‘(𝐴 ·
𝑁)) = (exp‘(𝑁 · 𝐴))) | 
| 5 |  | oveq2 7439 | . . . . . 6
⊢ (𝑗 = 0 → (𝐴 · 𝑗) = (𝐴 · 0)) | 
| 6 | 5 | fveq2d 6910 | . . . . 5
⊢ (𝑗 = 0 → (exp‘(𝐴 · 𝑗)) = (exp‘(𝐴 · 0))) | 
| 7 |  | oveq2 7439 | . . . . 5
⊢ (𝑗 = 0 → ((exp‘𝐴)↑𝑗) = ((exp‘𝐴)↑0)) | 
| 8 | 6, 7 | eqeq12d 2753 | . . . 4
⊢ (𝑗 = 0 → ((exp‘(𝐴 · 𝑗)) = ((exp‘𝐴)↑𝑗) ↔ (exp‘(𝐴 · 0)) = ((exp‘𝐴)↑0))) | 
| 9 |  | oveq2 7439 | . . . . . 6
⊢ (𝑗 = 𝑘 → (𝐴 · 𝑗) = (𝐴 · 𝑘)) | 
| 10 | 9 | fveq2d 6910 | . . . . 5
⊢ (𝑗 = 𝑘 → (exp‘(𝐴 · 𝑗)) = (exp‘(𝐴 · 𝑘))) | 
| 11 |  | oveq2 7439 | . . . . 5
⊢ (𝑗 = 𝑘 → ((exp‘𝐴)↑𝑗) = ((exp‘𝐴)↑𝑘)) | 
| 12 | 10, 11 | eqeq12d 2753 | . . . 4
⊢ (𝑗 = 𝑘 → ((exp‘(𝐴 · 𝑗)) = ((exp‘𝐴)↑𝑗) ↔ (exp‘(𝐴 · 𝑘)) = ((exp‘𝐴)↑𝑘))) | 
| 13 |  | oveq2 7439 | . . . . . 6
⊢ (𝑗 = (𝑘 + 1) → (𝐴 · 𝑗) = (𝐴 · (𝑘 + 1))) | 
| 14 | 13 | fveq2d 6910 | . . . . 5
⊢ (𝑗 = (𝑘 + 1) → (exp‘(𝐴 · 𝑗)) = (exp‘(𝐴 · (𝑘 + 1)))) | 
| 15 |  | oveq2 7439 | . . . . 5
⊢ (𝑗 = (𝑘 + 1) → ((exp‘𝐴)↑𝑗) = ((exp‘𝐴)↑(𝑘 + 1))) | 
| 16 | 14, 15 | eqeq12d 2753 | . . . 4
⊢ (𝑗 = (𝑘 + 1) → ((exp‘(𝐴 · 𝑗)) = ((exp‘𝐴)↑𝑗) ↔ (exp‘(𝐴 · (𝑘 + 1))) = ((exp‘𝐴)↑(𝑘 + 1)))) | 
| 17 |  | oveq2 7439 | . . . . . 6
⊢ (𝑗 = -𝑘 → (𝐴 · 𝑗) = (𝐴 · -𝑘)) | 
| 18 | 17 | fveq2d 6910 | . . . . 5
⊢ (𝑗 = -𝑘 → (exp‘(𝐴 · 𝑗)) = (exp‘(𝐴 · -𝑘))) | 
| 19 |  | oveq2 7439 | . . . . 5
⊢ (𝑗 = -𝑘 → ((exp‘𝐴)↑𝑗) = ((exp‘𝐴)↑-𝑘)) | 
| 20 | 18, 19 | eqeq12d 2753 | . . . 4
⊢ (𝑗 = -𝑘 → ((exp‘(𝐴 · 𝑗)) = ((exp‘𝐴)↑𝑗) ↔ (exp‘(𝐴 · -𝑘)) = ((exp‘𝐴)↑-𝑘))) | 
| 21 |  | oveq2 7439 | . . . . . 6
⊢ (𝑗 = 𝑁 → (𝐴 · 𝑗) = (𝐴 · 𝑁)) | 
| 22 | 21 | fveq2d 6910 | . . . . 5
⊢ (𝑗 = 𝑁 → (exp‘(𝐴 · 𝑗)) = (exp‘(𝐴 · 𝑁))) | 
| 23 |  | oveq2 7439 | . . . . 5
⊢ (𝑗 = 𝑁 → ((exp‘𝐴)↑𝑗) = ((exp‘𝐴)↑𝑁)) | 
| 24 | 22, 23 | eqeq12d 2753 | . . . 4
⊢ (𝑗 = 𝑁 → ((exp‘(𝐴 · 𝑗)) = ((exp‘𝐴)↑𝑗) ↔ (exp‘(𝐴 · 𝑁)) = ((exp‘𝐴)↑𝑁))) | 
| 25 |  | ef0 16127 | . . . . 5
⊢
(exp‘0) = 1 | 
| 26 |  | mul01 11440 | . . . . . 6
⊢ (𝐴 ∈ ℂ → (𝐴 · 0) =
0) | 
| 27 | 26 | fveq2d 6910 | . . . . 5
⊢ (𝐴 ∈ ℂ →
(exp‘(𝐴 · 0))
= (exp‘0)) | 
| 28 |  | efcl 16118 | . . . . . 6
⊢ (𝐴 ∈ ℂ →
(exp‘𝐴) ∈
ℂ) | 
| 29 | 28 | exp0d 14180 | . . . . 5
⊢ (𝐴 ∈ ℂ →
((exp‘𝐴)↑0) =
1) | 
| 30 | 25, 27, 29 | 3eqtr4a 2803 | . . . 4
⊢ (𝐴 ∈ ℂ →
(exp‘(𝐴 · 0))
= ((exp‘𝐴)↑0)) | 
| 31 |  | oveq1 7438 | . . . . . . 7
⊢
((exp‘(𝐴
· 𝑘)) =
((exp‘𝐴)↑𝑘) → ((exp‘(𝐴 · 𝑘)) · (exp‘𝐴)) = (((exp‘𝐴)↑𝑘) · (exp‘𝐴))) | 
| 32 | 31 | adantl 481 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
∧ (exp‘(𝐴
· 𝑘)) =
((exp‘𝐴)↑𝑘)) → ((exp‘(𝐴 · 𝑘)) · (exp‘𝐴)) = (((exp‘𝐴)↑𝑘) · (exp‘𝐴))) | 
| 33 |  | nn0cn 12536 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℂ) | 
| 34 |  | ax-1cn 11213 | . . . . . . . . . . . 12
⊢ 1 ∈
ℂ | 
| 35 |  | adddi 11244 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ ∧ 1 ∈
ℂ) → (𝐴 ·
(𝑘 + 1)) = ((𝐴 · 𝑘) + (𝐴 · 1))) | 
| 36 | 34, 35 | mp3an3 1452 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝐴 · (𝑘 + 1)) = ((𝐴 · 𝑘) + (𝐴 · 1))) | 
| 37 |  | mulrid 11259 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴) | 
| 38 | 37 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝐴 · 1) = 𝐴) | 
| 39 | 38 | oveq2d 7447 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝐴 · 𝑘) + (𝐴 · 1)) = ((𝐴 · 𝑘) + 𝐴)) | 
| 40 | 36, 39 | eqtrd 2777 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝐴 · (𝑘 + 1)) = ((𝐴 · 𝑘) + 𝐴)) | 
| 41 | 33, 40 | sylan2 593 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐴 · (𝑘 + 1)) = ((𝐴 · 𝑘) + 𝐴)) | 
| 42 | 41 | fveq2d 6910 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (exp‘(𝐴
· (𝑘 + 1))) =
(exp‘((𝐴 ·
𝑘) + 𝐴))) | 
| 43 |  | mulcl 11239 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝐴 · 𝑘) ∈ ℂ) | 
| 44 | 33, 43 | sylan2 593 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐴 · 𝑘) ∈
ℂ) | 
| 45 |  | simpl 482 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ 𝐴 ∈
ℂ) | 
| 46 |  | efadd 16130 | . . . . . . . . 9
⊢ (((𝐴 · 𝑘) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (exp‘((𝐴 · 𝑘) + 𝐴)) = ((exp‘(𝐴 · 𝑘)) · (exp‘𝐴))) | 
| 47 | 44, 45, 46 | syl2anc 584 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (exp‘((𝐴
· 𝑘) + 𝐴)) = ((exp‘(𝐴 · 𝑘)) · (exp‘𝐴))) | 
| 48 | 42, 47 | eqtrd 2777 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (exp‘(𝐴
· (𝑘 + 1))) =
((exp‘(𝐴 ·
𝑘)) ·
(exp‘𝐴))) | 
| 49 | 48 | adantr 480 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
∧ (exp‘(𝐴
· 𝑘)) =
((exp‘𝐴)↑𝑘)) → (exp‘(𝐴 · (𝑘 + 1))) = ((exp‘(𝐴 · 𝑘)) · (exp‘𝐴))) | 
| 50 |  | expp1 14109 | . . . . . . . 8
⊢
(((exp‘𝐴)
∈ ℂ ∧ 𝑘
∈ ℕ0) → ((exp‘𝐴)↑(𝑘 + 1)) = (((exp‘𝐴)↑𝑘) · (exp‘𝐴))) | 
| 51 | 28, 50 | sylan 580 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ ((exp‘𝐴)↑(𝑘 + 1)) = (((exp‘𝐴)↑𝑘) · (exp‘𝐴))) | 
| 52 | 51 | adantr 480 | . . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
∧ (exp‘(𝐴
· 𝑘)) =
((exp‘𝐴)↑𝑘)) → ((exp‘𝐴)↑(𝑘 + 1)) = (((exp‘𝐴)↑𝑘) · (exp‘𝐴))) | 
| 53 | 32, 49, 52 | 3eqtr4d 2787 | . . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
∧ (exp‘(𝐴
· 𝑘)) =
((exp‘𝐴)↑𝑘)) → (exp‘(𝐴 · (𝑘 + 1))) = ((exp‘𝐴)↑(𝑘 + 1))) | 
| 54 | 53 | exp31 419 | . . . 4
⊢ (𝐴 ∈ ℂ → (𝑘 ∈ ℕ0
→ ((exp‘(𝐴
· 𝑘)) =
((exp‘𝐴)↑𝑘) → (exp‘(𝐴 · (𝑘 + 1))) = ((exp‘𝐴)↑(𝑘 + 1))))) | 
| 55 |  | oveq2 7439 | . . . . . 6
⊢
((exp‘(𝐴
· 𝑘)) =
((exp‘𝐴)↑𝑘) → (1 / (exp‘(𝐴 · 𝑘))) = (1 / ((exp‘𝐴)↑𝑘))) | 
| 56 |  | nncn 12274 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) | 
| 57 |  | mulneg2 11700 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (𝐴 · -𝑘) = -(𝐴 · 𝑘)) | 
| 58 | 56, 57 | sylan2 593 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ) → (𝐴 · -𝑘) = -(𝐴 · 𝑘)) | 
| 59 | 58 | fveq2d 6910 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ) →
(exp‘(𝐴 ·
-𝑘)) = (exp‘-(𝐴 · 𝑘))) | 
| 60 | 56, 43 | sylan2 593 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ) → (𝐴 · 𝑘) ∈ ℂ) | 
| 61 |  | efneg 16134 | . . . . . . . . 9
⊢ ((𝐴 · 𝑘) ∈ ℂ → (exp‘-(𝐴 · 𝑘)) = (1 / (exp‘(𝐴 · 𝑘)))) | 
| 62 | 60, 61 | syl 17 | . . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ) →
(exp‘-(𝐴 ·
𝑘)) = (1 /
(exp‘(𝐴 ·
𝑘)))) | 
| 63 | 59, 62 | eqtrd 2777 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ) →
(exp‘(𝐴 ·
-𝑘)) = (1 /
(exp‘(𝐴 ·
𝑘)))) | 
| 64 |  | nnnn0 12533 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) | 
| 65 |  | expneg 14110 | . . . . . . . 8
⊢
(((exp‘𝐴)
∈ ℂ ∧ 𝑘
∈ ℕ0) → ((exp‘𝐴)↑-𝑘) = (1 / ((exp‘𝐴)↑𝑘))) | 
| 66 | 28, 64, 65 | syl2an 596 | . . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ) →
((exp‘𝐴)↑-𝑘) = (1 / ((exp‘𝐴)↑𝑘))) | 
| 67 | 63, 66 | eqeq12d 2753 | . . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ) →
((exp‘(𝐴 ·
-𝑘)) = ((exp‘𝐴)↑-𝑘) ↔ (1 / (exp‘(𝐴 · 𝑘))) = (1 / ((exp‘𝐴)↑𝑘)))) | 
| 68 | 55, 67 | imbitrrid 246 | . . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ) →
((exp‘(𝐴 ·
𝑘)) = ((exp‘𝐴)↑𝑘) → (exp‘(𝐴 · -𝑘)) = ((exp‘𝐴)↑-𝑘))) | 
| 69 | 68 | ex 412 | . . . 4
⊢ (𝐴 ∈ ℂ → (𝑘 ∈ ℕ →
((exp‘(𝐴 ·
𝑘)) = ((exp‘𝐴)↑𝑘) → (exp‘(𝐴 · -𝑘)) = ((exp‘𝐴)↑-𝑘)))) | 
| 70 | 8, 12, 16, 20, 24, 30, 54, 69 | zindd 12719 | . . 3
⊢ (𝐴 ∈ ℂ → (𝑁 ∈ ℤ →
(exp‘(𝐴 ·
𝑁)) = ((exp‘𝐴)↑𝑁))) | 
| 71 | 70 | imp 406 | . 2
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) →
(exp‘(𝐴 ·
𝑁)) = ((exp‘𝐴)↑𝑁)) | 
| 72 | 4, 71 | eqtr3d 2779 | 1
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) →
(exp‘(𝑁 ·
𝐴)) = ((exp‘𝐴)↑𝑁)) |