| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dvply1.f | . . 3
⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))) | 
| 2 | 1 | oveq2d 7447 | . 2
⊢ (𝜑 → (ℂ D 𝐹) = (ℂ D (𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))))) | 
| 3 |  | eqid 2737 | . . . . 5
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) | 
| 4 | 3 | cnfldtopon 24803 | . . . 4
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) | 
| 5 | 4 | toponrestid 22927 | . . 3
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) | 
| 6 |  | cnelprrecn 11248 | . . . 4
⊢ ℂ
∈ {ℝ, ℂ} | 
| 7 | 6 | a1i 11 | . . 3
⊢ (𝜑 → ℂ ∈ {ℝ,
ℂ}) | 
| 8 | 3 | cnfldtop 24804 | . . . 4
⊢
(TopOpen‘ℂfld) ∈ Top | 
| 9 |  | unicntop 24806 | . . . . 5
⊢ ℂ =
∪
(TopOpen‘ℂfld) | 
| 10 | 9 | topopn 22912 | . . . 4
⊢
((TopOpen‘ℂfld) ∈ Top → ℂ ∈
(TopOpen‘ℂfld)) | 
| 11 | 8, 10 | mp1i 13 | . . 3
⊢ (𝜑 → ℂ ∈
(TopOpen‘ℂfld)) | 
| 12 |  | fzfid 14014 | . . 3
⊢ (𝜑 → (0...𝑁) ∈ Fin) | 
| 13 |  | dvply1.a | . . . . . . 7
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) | 
| 14 |  | elfznn0 13660 | . . . . . . 7
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) | 
| 15 |  | ffvelcdm 7101 | . . . . . . 7
⊢ ((𝐴:ℕ0⟶ℂ ∧
𝑘 ∈
ℕ0) → (𝐴‘𝑘) ∈ ℂ) | 
| 16 | 13, 14, 15 | syl2an 596 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴‘𝑘) ∈ ℂ) | 
| 17 | 16 | adantr 480 | . . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑧 ∈ ℂ) → (𝐴‘𝑘) ∈ ℂ) | 
| 18 |  | simpr 484 | . . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑧 ∈ ℂ) → 𝑧 ∈ ℂ) | 
| 19 | 14 | ad2antlr 727 | . . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑧 ∈ ℂ) → 𝑘 ∈ ℕ0) | 
| 20 | 18, 19 | expcld 14186 | . . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑧 ∈ ℂ) → (𝑧↑𝑘) ∈ ℂ) | 
| 21 | 17, 20 | mulcld 11281 | . . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑧 ∈ ℂ) → ((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) | 
| 22 | 21 | 3impa 1110 | . . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) → ((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) | 
| 23 | 16 | 3adant3 1133 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) → (𝐴‘𝑘) ∈ ℂ) | 
| 24 |  | 0cnd 11254 | . . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 = 0) → 0 ∈
ℂ) | 
| 25 |  | simpl2 1193 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → 𝑘 ∈ (0...𝑁)) | 
| 26 | 25, 14 | syl 17 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → 𝑘 ∈ ℕ0) | 
| 27 | 26 | nn0cnd 12589 | . . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → 𝑘 ∈ ℂ) | 
| 28 |  | simpl3 1194 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → 𝑧 ∈ ℂ) | 
| 29 |  | simpr 484 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → ¬ 𝑘 = 0) | 
| 30 |  | elnn0 12528 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
↔ (𝑘 ∈ ℕ
∨ 𝑘 =
0)) | 
| 31 | 26, 30 | sylib 218 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → (𝑘 ∈ ℕ ∨ 𝑘 = 0)) | 
| 32 |  | orel2 891 | . . . . . . . . 9
⊢ (¬
𝑘 = 0 → ((𝑘 ∈ ℕ ∨ 𝑘 = 0) → 𝑘 ∈ ℕ)) | 
| 33 | 29, 31, 32 | sylc 65 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → 𝑘 ∈ ℕ) | 
| 34 |  | nnm1nn0 12567 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ → (𝑘 − 1) ∈
ℕ0) | 
| 35 | 33, 34 | syl 17 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → (𝑘 − 1) ∈
ℕ0) | 
| 36 | 28, 35 | expcld 14186 | . . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → (𝑧↑(𝑘 − 1)) ∈ ℂ) | 
| 37 | 27, 36 | mulcld 11281 | . . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → (𝑘 · (𝑧↑(𝑘 − 1))) ∈
ℂ) | 
| 38 | 24, 37 | ifclda 4561 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) → if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))) ∈
ℂ) | 
| 39 | 23, 38 | mulcld 11281 | . . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) → ((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))) ∈
ℂ) | 
| 40 | 6 | a1i 11 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ℂ ∈ {ℝ,
ℂ}) | 
| 41 |  | c0ex 11255 | . . . . . 6
⊢ 0 ∈
V | 
| 42 |  | ovex 7464 | . . . . . 6
⊢ (𝑘 · (𝑧↑(𝑘 − 1))) ∈ V | 
| 43 | 41, 42 | ifex 4576 | . . . . 5
⊢ if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))) ∈ V | 
| 44 | 43 | a1i 11 | . . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑧 ∈ ℂ) → if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))) ∈ V) | 
| 45 | 14 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0) | 
| 46 |  | dvexp2 25992 | . . . . 5
⊢ (𝑘 ∈ ℕ0
→ (ℂ D (𝑧 ∈
ℂ ↦ (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))))) | 
| 47 | 45, 46 | syl 17 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (ℂ D (𝑧 ∈ ℂ ↦ (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))))) | 
| 48 | 40, 20, 44, 47, 16 | dvmptcmul 26002 | . . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (ℂ D (𝑧 ∈ ℂ ↦ ((𝐴‘𝑘) · (𝑧↑𝑘)))) = (𝑧 ∈ ℂ ↦ ((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))))) | 
| 49 | 5, 3, 7, 11, 12, 22, 39, 48 | dvmptfsum 26013 | . 2
⊢ (𝜑 → (ℂ D (𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))))) | 
| 50 |  | elfznn 13593 | . . . . . . . . . . 11
⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℕ) | 
| 51 | 50 | nnne0d 12316 | . . . . . . . . . 10
⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ≠ 0) | 
| 52 | 51 | neneqd 2945 | . . . . . . . . 9
⊢ (𝑘 ∈ (1...𝑁) → ¬ 𝑘 = 0) | 
| 53 | 52 | adantl 481 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → ¬ 𝑘 = 0) | 
| 54 | 53 | iffalsed 4536 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))) = (𝑘 · (𝑧↑(𝑘 − 1)))) | 
| 55 | 54 | oveq2d 7447 | . . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → ((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))) = ((𝐴‘𝑘) · (𝑘 · (𝑧↑(𝑘 − 1))))) | 
| 56 | 55 | sumeq2dv 15738 | . . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (1...𝑁)((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))) = Σ𝑘 ∈ (1...𝑁)((𝐴‘𝑘) · (𝑘 · (𝑧↑(𝑘 − 1))))) | 
| 57 |  | 1eluzge0 12934 | . . . . . . 7
⊢ 1 ∈
(ℤ≥‘0) | 
| 58 |  | fzss1 13603 | . . . . . . 7
⊢ (1 ∈
(ℤ≥‘0) → (1...𝑁) ⊆ (0...𝑁)) | 
| 59 | 57, 58 | mp1i 13 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (1...𝑁) ⊆ (0...𝑁)) | 
| 60 | 13 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝐴:ℕ0⟶ℂ) | 
| 61 | 50 | nnnn0d 12587 | . . . . . . . 8
⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℕ0) | 
| 62 | 60, 61, 15 | syl2an 596 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → (𝐴‘𝑘) ∈ ℂ) | 
| 63 | 51 | adantl 481 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → 𝑘 ≠ 0) | 
| 64 | 63 | neneqd 2945 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → ¬ 𝑘 = 0) | 
| 65 | 64 | iffalsed 4536 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))) = (𝑘 · (𝑧↑(𝑘 − 1)))) | 
| 66 | 61 | adantl 481 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → 𝑘 ∈ ℕ0) | 
| 67 | 66 | nn0cnd 12589 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → 𝑘 ∈ ℂ) | 
| 68 |  | simplr 769 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → 𝑧 ∈ ℂ) | 
| 69 | 50, 34 | syl 17 | . . . . . . . . . . 11
⊢ (𝑘 ∈ (1...𝑁) → (𝑘 − 1) ∈
ℕ0) | 
| 70 | 69 | adantl 481 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → (𝑘 − 1) ∈
ℕ0) | 
| 71 | 68, 70 | expcld 14186 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → (𝑧↑(𝑘 − 1)) ∈ ℂ) | 
| 72 | 67, 71 | mulcld 11281 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → (𝑘 · (𝑧↑(𝑘 − 1))) ∈
ℂ) | 
| 73 | 65, 72 | eqeltrd 2841 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))) ∈
ℂ) | 
| 74 | 62, 73 | mulcld 11281 | . . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → ((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))) ∈
ℂ) | 
| 75 |  | eldifn 4132 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ ((0...𝑁) ∖ (1...𝑁)) → ¬ 𝑘 ∈ (1...𝑁)) | 
| 76 |  | 0p1e1 12388 | . . . . . . . . . . . . . 14
⊢ (0 + 1) =
1 | 
| 77 | 76 | oveq1i 7441 | . . . . . . . . . . . . 13
⊢ ((0 +
1)...𝑁) = (1...𝑁) | 
| 78 | 77 | eleq2i 2833 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ ((0 + 1)...𝑁) ↔ 𝑘 ∈ (1...𝑁)) | 
| 79 | 75, 78 | sylnibr 329 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ((0...𝑁) ∖ (1...𝑁)) → ¬ 𝑘 ∈ ((0 + 1)...𝑁)) | 
| 80 | 79 | adantl 481 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → ¬ 𝑘 ∈ ((0 + 1)...𝑁)) | 
| 81 |  | eldifi 4131 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ ((0...𝑁) ∖ (1...𝑁)) → 𝑘 ∈ (0...𝑁)) | 
| 82 | 81 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → 𝑘 ∈ (0...𝑁)) | 
| 83 |  | dvply1.n | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 84 |  | nn0uz 12920 | . . . . . . . . . . . . . 14
⊢
ℕ0 = (ℤ≥‘0) | 
| 85 | 83, 84 | eleqtrdi 2851 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘0)) | 
| 86 | 85 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → 𝑁 ∈
(ℤ≥‘0)) | 
| 87 |  | elfzp12 13643 | . . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘0) → (𝑘 ∈ (0...𝑁) ↔ (𝑘 = 0 ∨ 𝑘 ∈ ((0 + 1)...𝑁)))) | 
| 88 | 86, 87 | syl 17 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → (𝑘 ∈ (0...𝑁) ↔ (𝑘 = 0 ∨ 𝑘 ∈ ((0 + 1)...𝑁)))) | 
| 89 | 82, 88 | mpbid 232 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → (𝑘 = 0 ∨ 𝑘 ∈ ((0 + 1)...𝑁))) | 
| 90 |  | orel2 891 | . . . . . . . . . 10
⊢ (¬
𝑘 ∈ ((0 + 1)...𝑁) → ((𝑘 = 0 ∨ 𝑘 ∈ ((0 + 1)...𝑁)) → 𝑘 = 0)) | 
| 91 | 80, 89, 90 | sylc 65 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → 𝑘 = 0) | 
| 92 | 91 | iftrued 4533 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))) = 0) | 
| 93 | 92 | oveq2d 7447 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → ((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))) = ((𝐴‘𝑘) · 0)) | 
| 94 | 60, 14, 15 | syl2an 596 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → (𝐴‘𝑘) ∈ ℂ) | 
| 95 | 94 | mul01d 11460 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴‘𝑘) · 0) = 0) | 
| 96 | 81, 95 | sylan2 593 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → ((𝐴‘𝑘) · 0) = 0) | 
| 97 | 93, 96 | eqtrd 2777 | . . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → ((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))) = 0) | 
| 98 |  | fzfid 14014 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (0...𝑁) ∈ Fin) | 
| 99 | 59, 74, 97, 98 | fsumss 15761 | . . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (1...𝑁)((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))))) | 
| 100 |  | elfznn0 13660 | . . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 ∈ ℕ0) | 
| 101 | 100 | adantl 481 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑗 ∈ ℕ0) | 
| 102 | 101 | nn0cnd 12589 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑗 ∈ ℂ) | 
| 103 |  | ax-1cn 11213 | . . . . . . . . . . . . 13
⊢ 1 ∈
ℂ | 
| 104 |  | pncan 11514 | . . . . . . . . . . . . 13
⊢ ((𝑗 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑗 + 1)
− 1) = 𝑗) | 
| 105 | 102, 103,
104 | sylancl 586 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑗 + 1) − 1) = 𝑗) | 
| 106 | 105 | oveq2d 7447 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑧↑((𝑗 + 1) − 1)) = (𝑧↑𝑗)) | 
| 107 | 106 | oveq2d 7447 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1))) = ((𝑗 + 1) · (𝑧↑𝑗))) | 
| 108 | 107 | oveq2d 7447 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1)))) = ((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑𝑗)))) | 
| 109 | 13 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝐴:ℕ0⟶ℂ) | 
| 110 |  | peano2nn0 12566 | . . . . . . . . . . . . 13
⊢ (𝑗 ∈ ℕ0
→ (𝑗 + 1) ∈
ℕ0) | 
| 111 | 100, 110 | syl 17 | . . . . . . . . . . . 12
⊢ (𝑗 ∈ (0...(𝑁 − 1)) → (𝑗 + 1) ∈
ℕ0) | 
| 112 | 111 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑗 + 1) ∈
ℕ0) | 
| 113 | 109, 112 | ffvelcdmd 7105 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝐴‘(𝑗 + 1)) ∈ ℂ) | 
| 114 | 112 | nn0cnd 12589 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑗 + 1) ∈ ℂ) | 
| 115 |  | simplr 769 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑧 ∈ ℂ) | 
| 116 | 115, 101 | expcld 14186 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑧↑𝑗) ∈ ℂ) | 
| 117 | 113, 114,
116 | mulassd 11284 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (((𝐴‘(𝑗 + 1)) · (𝑗 + 1)) · (𝑧↑𝑗)) = ((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑𝑗)))) | 
| 118 | 113, 114 | mulcomd 11282 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝐴‘(𝑗 + 1)) · (𝑗 + 1)) = ((𝑗 + 1) · (𝐴‘(𝑗 + 1)))) | 
| 119 | 118 | oveq1d 7446 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (((𝐴‘(𝑗 + 1)) · (𝑗 + 1)) · (𝑧↑𝑗)) = (((𝑗 + 1) · (𝐴‘(𝑗 + 1))) · (𝑧↑𝑗))) | 
| 120 | 108, 117,
119 | 3eqtr2d 2783 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1)))) = (((𝑗 + 1) · (𝐴‘(𝑗 + 1))) · (𝑧↑𝑗))) | 
| 121 | 120 | sumeq2dv 15738 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑗 ∈ (0...(𝑁 − 1))((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1)))) = Σ𝑗 ∈ (0...(𝑁 − 1))(((𝑗 + 1) · (𝐴‘(𝑗 + 1))) · (𝑧↑𝑗))) | 
| 122 |  | 1m1e0 12338 | . . . . . . . . 9
⊢ (1
− 1) = 0 | 
| 123 | 122 | oveq1i 7441 | . . . . . . . 8
⊢ ((1
− 1)...(𝑁 − 1))
= (0...(𝑁 −
1)) | 
| 124 | 123 | sumeq1i 15733 | . . . . . . 7
⊢
Σ𝑗 ∈ ((1
− 1)...(𝑁 −
1))((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1)))) = Σ𝑗 ∈ (0...(𝑁 − 1))((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1)))) | 
| 125 |  | oveq1 7438 | . . . . . . . . . 10
⊢ (𝑘 = 𝑗 → (𝑘 + 1) = (𝑗 + 1)) | 
| 126 |  | fvoveq1 7454 | . . . . . . . . . 10
⊢ (𝑘 = 𝑗 → (𝐴‘(𝑘 + 1)) = (𝐴‘(𝑗 + 1))) | 
| 127 | 125, 126 | oveq12d 7449 | . . . . . . . . 9
⊢ (𝑘 = 𝑗 → ((𝑘 + 1) · (𝐴‘(𝑘 + 1))) = ((𝑗 + 1) · (𝐴‘(𝑗 + 1)))) | 
| 128 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑘 = 𝑗 → (𝑧↑𝑘) = (𝑧↑𝑗)) | 
| 129 | 127, 128 | oveq12d 7449 | . . . . . . . 8
⊢ (𝑘 = 𝑗 → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑧↑𝑘)) = (((𝑗 + 1) · (𝐴‘(𝑗 + 1))) · (𝑧↑𝑗))) | 
| 130 | 129 | cbvsumv 15732 | . . . . . . 7
⊢
Σ𝑘 ∈
(0...(𝑁 − 1))(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑧↑𝑘)) = Σ𝑗 ∈ (0...(𝑁 − 1))(((𝑗 + 1) · (𝐴‘(𝑗 + 1))) · (𝑧↑𝑗)) | 
| 131 | 121, 124,
130 | 3eqtr4g 2802 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑗 ∈ ((1 − 1)...(𝑁 − 1))((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1)))) = Σ𝑘 ∈ (0...(𝑁 − 1))(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑧↑𝑘))) | 
| 132 |  | 1zzd 12648 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 1 ∈
ℤ) | 
| 133 | 83 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝑁 ∈
ℕ0) | 
| 134 | 133 | nn0zd 12639 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝑁 ∈ ℤ) | 
| 135 | 62, 72 | mulcld 11281 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → ((𝐴‘𝑘) · (𝑘 · (𝑧↑(𝑘 − 1)))) ∈
ℂ) | 
| 136 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑘 = (𝑗 + 1) → (𝐴‘𝑘) = (𝐴‘(𝑗 + 1))) | 
| 137 |  | id 22 | . . . . . . . . 9
⊢ (𝑘 = (𝑗 + 1) → 𝑘 = (𝑗 + 1)) | 
| 138 |  | oveq1 7438 | . . . . . . . . . 10
⊢ (𝑘 = (𝑗 + 1) → (𝑘 − 1) = ((𝑗 + 1) − 1)) | 
| 139 | 138 | oveq2d 7447 | . . . . . . . . 9
⊢ (𝑘 = (𝑗 + 1) → (𝑧↑(𝑘 − 1)) = (𝑧↑((𝑗 + 1) − 1))) | 
| 140 | 137, 139 | oveq12d 7449 | . . . . . . . 8
⊢ (𝑘 = (𝑗 + 1) → (𝑘 · (𝑧↑(𝑘 − 1))) = ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1)))) | 
| 141 | 136, 140 | oveq12d 7449 | . . . . . . 7
⊢ (𝑘 = (𝑗 + 1) → ((𝐴‘𝑘) · (𝑘 · (𝑧↑(𝑘 − 1)))) = ((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1))))) | 
| 142 | 132, 132,
134, 135, 141 | fsumshftm 15817 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (1...𝑁)((𝐴‘𝑘) · (𝑘 · (𝑧↑(𝑘 − 1)))) = Σ𝑗 ∈ ((1 − 1)...(𝑁 − 1))((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1))))) | 
| 143 |  | elfznn0 13660 | . . . . . . . . . 10
⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ0) | 
| 144 | 143 | adantl 481 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ ℕ0) | 
| 145 |  | ovex 7464 | . . . . . . . . 9
⊢ ((𝑘 + 1) · (𝐴‘(𝑘 + 1))) ∈ V | 
| 146 |  | dvply1.b | . . . . . . . . . 10
⊢ 𝐵 = (𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) · (𝐴‘(𝑘 + 1)))) | 
| 147 | 146 | fvmpt2 7027 | . . . . . . . . 9
⊢ ((𝑘 ∈ ℕ0
∧ ((𝑘 + 1) ·
(𝐴‘(𝑘 + 1))) ∈ V) → (𝐵‘𝑘) = ((𝑘 + 1) · (𝐴‘(𝑘 + 1)))) | 
| 148 | 144, 145,
147 | sylancl 586 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐵‘𝑘) = ((𝑘 + 1) · (𝐴‘(𝑘 + 1)))) | 
| 149 | 148 | oveq1d 7446 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝐵‘𝑘) · (𝑧↑𝑘)) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑧↑𝑘))) | 
| 150 | 149 | sumeq2dv 15738 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...(𝑁 − 1))((𝐵‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...(𝑁 − 1))(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑧↑𝑘))) | 
| 151 | 131, 142,
150 | 3eqtr4d 2787 | . . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (1...𝑁)((𝐴‘𝑘) · (𝑘 · (𝑧↑(𝑘 − 1)))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝐵‘𝑘) · (𝑧↑𝑘))) | 
| 152 | 56, 99, 151 | 3eqtr3d 2785 | . . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝐵‘𝑘) · (𝑧↑𝑘))) | 
| 153 | 152 | mpteq2dva 5242 | . . 3
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(𝑁 − 1))((𝐵‘𝑘) · (𝑧↑𝑘)))) | 
| 154 |  | dvply1.g | . . 3
⊢ (𝜑 → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(𝑁 − 1))((𝐵‘𝑘) · (𝑧↑𝑘)))) | 
| 155 | 153, 154 | eqtr4d 2780 | . 2
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))))) = 𝐺) | 
| 156 | 2, 49, 155 | 3eqtrd 2781 | 1
⊢ (𝜑 → (ℂ D 𝐹) = 𝐺) |