Step | Hyp | Ref
| Expression |
1 | | dvply1.f |
. . 3
⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))) |
2 | 1 | oveq2d 7186 |
. 2
⊢ (𝜑 → (ℂ D 𝐹) = (ℂ D (𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))))) |
3 | | eqid 2738 |
. . . . 5
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
4 | 3 | cnfldtopon 23535 |
. . . 4
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
5 | 4 | toponrestid 21672 |
. . 3
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
6 | | cnelprrecn 10708 |
. . . 4
⊢ ℂ
∈ {ℝ, ℂ} |
7 | 6 | a1i 11 |
. . 3
⊢ (𝜑 → ℂ ∈ {ℝ,
ℂ}) |
8 | 3 | cnfldtop 23536 |
. . . 4
⊢
(TopOpen‘ℂfld) ∈ Top |
9 | | unicntop 23538 |
. . . . 5
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
10 | 9 | topopn 21657 |
. . . 4
⊢
((TopOpen‘ℂfld) ∈ Top → ℂ ∈
(TopOpen‘ℂfld)) |
11 | 8, 10 | mp1i 13 |
. . 3
⊢ (𝜑 → ℂ ∈
(TopOpen‘ℂfld)) |
12 | | fzfid 13432 |
. . 3
⊢ (𝜑 → (0...𝑁) ∈ Fin) |
13 | | dvply1.a |
. . . . . . 7
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
14 | | elfznn0 13091 |
. . . . . . 7
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) |
15 | | ffvelrn 6859 |
. . . . . . 7
⊢ ((𝐴:ℕ0⟶ℂ ∧
𝑘 ∈
ℕ0) → (𝐴‘𝑘) ∈ ℂ) |
16 | 13, 14, 15 | syl2an 599 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴‘𝑘) ∈ ℂ) |
17 | 16 | adantr 484 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑧 ∈ ℂ) → (𝐴‘𝑘) ∈ ℂ) |
18 | | simpr 488 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑧 ∈ ℂ) → 𝑧 ∈ ℂ) |
19 | 14 | ad2antlr 727 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑧 ∈ ℂ) → 𝑘 ∈ ℕ0) |
20 | 18, 19 | expcld 13602 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑧 ∈ ℂ) → (𝑧↑𝑘) ∈ ℂ) |
21 | 17, 20 | mulcld 10739 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑧 ∈ ℂ) → ((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
22 | 21 | 3impa 1111 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) → ((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
23 | 16 | 3adant3 1133 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) → (𝐴‘𝑘) ∈ ℂ) |
24 | | 0cnd 10712 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 = 0) → 0 ∈
ℂ) |
25 | | simpl2 1193 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → 𝑘 ∈ (0...𝑁)) |
26 | 25, 14 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → 𝑘 ∈ ℕ0) |
27 | 26 | nn0cnd 12038 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → 𝑘 ∈ ℂ) |
28 | | simpl3 1194 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → 𝑧 ∈ ℂ) |
29 | | simpr 488 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → ¬ 𝑘 = 0) |
30 | | elnn0 11978 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
↔ (𝑘 ∈ ℕ
∨ 𝑘 =
0)) |
31 | 26, 30 | sylib 221 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → (𝑘 ∈ ℕ ∨ 𝑘 = 0)) |
32 | | orel2 890 |
. . . . . . . . 9
⊢ (¬
𝑘 = 0 → ((𝑘 ∈ ℕ ∨ 𝑘 = 0) → 𝑘 ∈ ℕ)) |
33 | 29, 31, 32 | sylc 65 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → 𝑘 ∈ ℕ) |
34 | | nnm1nn0 12017 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ → (𝑘 − 1) ∈
ℕ0) |
35 | 33, 34 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → (𝑘 − 1) ∈
ℕ0) |
36 | 28, 35 | expcld 13602 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → (𝑧↑(𝑘 − 1)) ∈ ℂ) |
37 | 27, 36 | mulcld 10739 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → (𝑘 · (𝑧↑(𝑘 − 1))) ∈
ℂ) |
38 | 24, 37 | ifclda 4449 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) → if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))) ∈
ℂ) |
39 | 23, 38 | mulcld 10739 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) → ((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))) ∈
ℂ) |
40 | 6 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ℂ ∈ {ℝ,
ℂ}) |
41 | | c0ex 10713 |
. . . . . 6
⊢ 0 ∈
V |
42 | | ovex 7203 |
. . . . . 6
⊢ (𝑘 · (𝑧↑(𝑘 − 1))) ∈ V |
43 | 41, 42 | ifex 4464 |
. . . . 5
⊢ if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))) ∈ V |
44 | 43 | a1i 11 |
. . . 4
⊢ (((𝜑 ∧ 𝑘 ∈ (0...𝑁)) ∧ 𝑧 ∈ ℂ) → if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))) ∈ V) |
45 | 14 | adantl 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0) |
46 | | dvexp2 24706 |
. . . . 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 24716 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (ℂ D (𝑧 ∈ ℂ ↦ ((𝐴‘𝑘) · (𝑧↑𝑘)))) = (𝑧 ∈ ℂ ↦ ((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))))) |
49 | 5, 3, 7, 11, 12, 22, 39, 48 | dvmptfsum 24727 |
. 2
⊢ (𝜑 → (ℂ D (𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘)))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))))) |
50 | | elfznn 13027 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℕ) |
51 | 50 | nnne0d 11766 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ≠ 0) |
52 | 51 | neneqd 2939 |
. . . . . . . . 9
⊢ (𝑘 ∈ (1...𝑁) → ¬ 𝑘 = 0) |
53 | 52 | adantl 485 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → ¬ 𝑘 = 0) |
54 | 53 | iffalsed 4425 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))) = (𝑘 · (𝑧↑(𝑘 − 1)))) |
55 | 54 | oveq2d 7186 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → ((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))) = ((𝐴‘𝑘) · (𝑘 · (𝑧↑(𝑘 − 1))))) |
56 | 55 | sumeq2dv 15153 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (1...𝑁)((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))) = Σ𝑘 ∈ (1...𝑁)((𝐴‘𝑘) · (𝑘 · (𝑧↑(𝑘 − 1))))) |
57 | | 1eluzge0 12374 |
. . . . . . 7
⊢ 1 ∈
(ℤ≥‘0) |
58 | | fzss1 13037 |
. . . . . . 7
⊢ (1 ∈
(ℤ≥‘0) → (1...𝑁) ⊆ (0...𝑁)) |
59 | 57, 58 | mp1i 13 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (1...𝑁) ⊆ (0...𝑁)) |
60 | 13 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝐴:ℕ0⟶ℂ) |
61 | 50 | nnnn0d 12036 |
. . . . . . . 8
⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℕ0) |
62 | 60, 61, 15 | syl2an 599 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → (𝐴‘𝑘) ∈ ℂ) |
63 | 51 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → 𝑘 ≠ 0) |
64 | 63 | neneqd 2939 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → ¬ 𝑘 = 0) |
65 | 64 | iffalsed 4425 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))) = (𝑘 · (𝑧↑(𝑘 − 1)))) |
66 | 61 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → 𝑘 ∈ ℕ0) |
67 | 66 | nn0cnd 12038 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → 𝑘 ∈ ℂ) |
68 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → 𝑧 ∈ ℂ) |
69 | 50, 34 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (1...𝑁) → (𝑘 − 1) ∈
ℕ0) |
70 | 69 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → (𝑘 − 1) ∈
ℕ0) |
71 | 68, 70 | expcld 13602 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → (𝑧↑(𝑘 − 1)) ∈ ℂ) |
72 | 67, 71 | mulcld 10739 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → (𝑘 · (𝑧↑(𝑘 − 1))) ∈
ℂ) |
73 | 65, 72 | eqeltrd 2833 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))) ∈
ℂ) |
74 | 62, 73 | mulcld 10739 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → ((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))) ∈
ℂ) |
75 | | eldifn 4018 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ((0...𝑁) ∖ (1...𝑁)) → ¬ 𝑘 ∈ (1...𝑁)) |
76 | | 0p1e1 11838 |
. . . . . . . . . . . . . 14
⊢ (0 + 1) =
1 |
77 | 76 | oveq1i 7180 |
. . . . . . . . . . . . 13
⊢ ((0 +
1)...𝑁) = (1...𝑁) |
78 | 77 | eleq2i 2824 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ((0 + 1)...𝑁) ↔ 𝑘 ∈ (1...𝑁)) |
79 | 75, 78 | sylnibr 332 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ((0...𝑁) ∖ (1...𝑁)) → ¬ 𝑘 ∈ ((0 + 1)...𝑁)) |
80 | 79 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → ¬ 𝑘 ∈ ((0 + 1)...𝑁)) |
81 | | eldifi 4017 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ((0...𝑁) ∖ (1...𝑁)) → 𝑘 ∈ (0...𝑁)) |
82 | 81 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → 𝑘 ∈ (0...𝑁)) |
83 | | dvply1.n |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
84 | | nn0uz 12362 |
. . . . . . . . . . . . . 14
⊢
ℕ0 = (ℤ≥‘0) |
85 | 83, 84 | eleqtrdi 2843 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘0)) |
86 | 85 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → 𝑁 ∈
(ℤ≥‘0)) |
87 | | elfzp12 13077 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘0) → (𝑘 ∈ (0...𝑁) ↔ (𝑘 = 0 ∨ 𝑘 ∈ ((0 + 1)...𝑁)))) |
88 | 86, 87 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → (𝑘 ∈ (0...𝑁) ↔ (𝑘 = 0 ∨ 𝑘 ∈ ((0 + 1)...𝑁)))) |
89 | 82, 88 | mpbid 235 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → (𝑘 = 0 ∨ 𝑘 ∈ ((0 + 1)...𝑁))) |
90 | | orel2 890 |
. . . . . . . . . 10
⊢ (¬
𝑘 ∈ ((0 + 1)...𝑁) → ((𝑘 = 0 ∨ 𝑘 ∈ ((0 + 1)...𝑁)) → 𝑘 = 0)) |
91 | 80, 89, 90 | sylc 65 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → 𝑘 = 0) |
92 | 91 | iftrued 4422 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))) = 0) |
93 | 92 | oveq2d 7186 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → ((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))) = ((𝐴‘𝑘) · 0)) |
94 | 60, 14, 15 | syl2an 599 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → (𝐴‘𝑘) ∈ ℂ) |
95 | 94 | mul01d 10917 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴‘𝑘) · 0) = 0) |
96 | 81, 95 | sylan2 596 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → ((𝐴‘𝑘) · 0) = 0) |
97 | 93, 96 | eqtrd 2773 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → ((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))) = 0) |
98 | | fzfid 13432 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (0...𝑁) ∈ Fin) |
99 | 59, 74, 97, 98 | fsumss 15175 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (1...𝑁)((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))))) |
100 | | elfznn0 13091 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 ∈ ℕ0) |
101 | 100 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑗 ∈ ℕ0) |
102 | 101 | nn0cnd 12038 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑗 ∈ ℂ) |
103 | | ax-1cn 10673 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
104 | | pncan 10970 |
. . . . . . . . . . . . 13
⊢ ((𝑗 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑗 + 1)
− 1) = 𝑗) |
105 | 102, 103,
104 | sylancl 589 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑗 + 1) − 1) = 𝑗) |
106 | 105 | oveq2d 7186 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑧↑((𝑗 + 1) − 1)) = (𝑧↑𝑗)) |
107 | 106 | oveq2d 7186 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1))) = ((𝑗 + 1) · (𝑧↑𝑗))) |
108 | 107 | oveq2d 7186 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1)))) = ((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑𝑗)))) |
109 | 13 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝐴:ℕ0⟶ℂ) |
110 | | peano2nn0 12016 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ℕ0
→ (𝑗 + 1) ∈
ℕ0) |
111 | 100, 110 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (0...(𝑁 − 1)) → (𝑗 + 1) ∈
ℕ0) |
112 | 111 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑗 + 1) ∈
ℕ0) |
113 | 109, 112 | ffvelrnd 6862 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝐴‘(𝑗 + 1)) ∈ ℂ) |
114 | 112 | nn0cnd 12038 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑗 + 1) ∈ ℂ) |
115 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑧 ∈ ℂ) |
116 | 115, 101 | expcld 13602 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑧↑𝑗) ∈ ℂ) |
117 | 113, 114,
116 | mulassd 10742 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (((𝐴‘(𝑗 + 1)) · (𝑗 + 1)) · (𝑧↑𝑗)) = ((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑𝑗)))) |
118 | 113, 114 | mulcomd 10740 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝐴‘(𝑗 + 1)) · (𝑗 + 1)) = ((𝑗 + 1) · (𝐴‘(𝑗 + 1)))) |
119 | 118 | oveq1d 7185 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (((𝐴‘(𝑗 + 1)) · (𝑗 + 1)) · (𝑧↑𝑗)) = (((𝑗 + 1) · (𝐴‘(𝑗 + 1))) · (𝑧↑𝑗))) |
120 | 108, 117,
119 | 3eqtr2d 2779 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1)))) = (((𝑗 + 1) · (𝐴‘(𝑗 + 1))) · (𝑧↑𝑗))) |
121 | 120 | sumeq2dv 15153 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑗 ∈ (0...(𝑁 − 1))((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1)))) = Σ𝑗 ∈ (0...(𝑁 − 1))(((𝑗 + 1) · (𝐴‘(𝑗 + 1))) · (𝑧↑𝑗))) |
122 | | 1m1e0 11788 |
. . . . . . . . 9
⊢ (1
− 1) = 0 |
123 | 122 | oveq1i 7180 |
. . . . . . . 8
⊢ ((1
− 1)...(𝑁 − 1))
= (0...(𝑁 −
1)) |
124 | 123 | sumeq1i 15148 |
. . . . . . 7
⊢
Σ𝑗 ∈ ((1
− 1)...(𝑁 −
1))((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1)))) = Σ𝑗 ∈ (0...(𝑁 − 1))((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1)))) |
125 | | oveq1 7177 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑗 → (𝑘 + 1) = (𝑗 + 1)) |
126 | | fvoveq1 7193 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑗 → (𝐴‘(𝑘 + 1)) = (𝐴‘(𝑗 + 1))) |
127 | 125, 126 | oveq12d 7188 |
. . . . . . . . 9
⊢ (𝑘 = 𝑗 → ((𝑘 + 1) · (𝐴‘(𝑘 + 1))) = ((𝑗 + 1) · (𝐴‘(𝑗 + 1)))) |
128 | | oveq2 7178 |
. . . . . . . . 9
⊢ (𝑘 = 𝑗 → (𝑧↑𝑘) = (𝑧↑𝑗)) |
129 | 127, 128 | oveq12d 7188 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑧↑𝑘)) = (((𝑗 + 1) · (𝐴‘(𝑗 + 1))) · (𝑧↑𝑗))) |
130 | 129 | cbvsumv 15146 |
. . . . . . 7
⊢
Σ𝑘 ∈
(0...(𝑁 − 1))(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑧↑𝑘)) = Σ𝑗 ∈ (0...(𝑁 − 1))(((𝑗 + 1) · (𝐴‘(𝑗 + 1))) · (𝑧↑𝑗)) |
131 | 121, 124,
130 | 3eqtr4g 2798 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑗 ∈ ((1 − 1)...(𝑁 − 1))((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1)))) = Σ𝑘 ∈ (0...(𝑁 − 1))(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑧↑𝑘))) |
132 | | 1zzd 12094 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 1 ∈
ℤ) |
133 | 83 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝑁 ∈
ℕ0) |
134 | 133 | nn0zd 12166 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝑁 ∈ ℤ) |
135 | 62, 72 | mulcld 10739 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → ((𝐴‘𝑘) · (𝑘 · (𝑧↑(𝑘 − 1)))) ∈
ℂ) |
136 | | fveq2 6674 |
. . . . . . . 8
⊢ (𝑘 = (𝑗 + 1) → (𝐴‘𝑘) = (𝐴‘(𝑗 + 1))) |
137 | | id 22 |
. . . . . . . . 9
⊢ (𝑘 = (𝑗 + 1) → 𝑘 = (𝑗 + 1)) |
138 | | oveq1 7177 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑗 + 1) → (𝑘 − 1) = ((𝑗 + 1) − 1)) |
139 | 138 | oveq2d 7186 |
. . . . . . . . 9
⊢ (𝑘 = (𝑗 + 1) → (𝑧↑(𝑘 − 1)) = (𝑧↑((𝑗 + 1) − 1))) |
140 | 137, 139 | oveq12d 7188 |
. . . . . . . 8
⊢ (𝑘 = (𝑗 + 1) → (𝑘 · (𝑧↑(𝑘 − 1))) = ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1)))) |
141 | 136, 140 | oveq12d 7188 |
. . . . . . 7
⊢ (𝑘 = (𝑗 + 1) → ((𝐴‘𝑘) · (𝑘 · (𝑧↑(𝑘 − 1)))) = ((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1))))) |
142 | 132, 132,
134, 135, 141 | fsumshftm 15229 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (1...𝑁)((𝐴‘𝑘) · (𝑘 · (𝑧↑(𝑘 − 1)))) = Σ𝑗 ∈ ((1 − 1)...(𝑁 − 1))((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1))))) |
143 | | elfznn0 13091 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ0) |
144 | 143 | adantl 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ ℕ0) |
145 | | ovex 7203 |
. . . . . . . . 9
⊢ ((𝑘 + 1) · (𝐴‘(𝑘 + 1))) ∈ V |
146 | | dvply1.b |
. . . . . . . . . 10
⊢ 𝐵 = (𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) · (𝐴‘(𝑘 + 1)))) |
147 | 146 | fvmpt2 6786 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ0
∧ ((𝑘 + 1) ·
(𝐴‘(𝑘 + 1))) ∈ V) → (𝐵‘𝑘) = ((𝑘 + 1) · (𝐴‘(𝑘 + 1)))) |
148 | 144, 145,
147 | sylancl 589 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐵‘𝑘) = ((𝑘 + 1) · (𝐴‘(𝑘 + 1)))) |
149 | 148 | oveq1d 7185 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝐵‘𝑘) · (𝑧↑𝑘)) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑧↑𝑘))) |
150 | 149 | sumeq2dv 15153 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...(𝑁 − 1))((𝐵‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...(𝑁 − 1))(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑧↑𝑘))) |
151 | 131, 142,
150 | 3eqtr4d 2783 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (1...𝑁)((𝐴‘𝑘) · (𝑘 · (𝑧↑(𝑘 − 1)))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝐵‘𝑘) · (𝑧↑𝑘))) |
152 | 56, 99, 151 | 3eqtr3d 2781 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝐵‘𝑘) · (𝑧↑𝑘))) |
153 | 152 | mpteq2dva 5125 |
. . 3
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(𝑁 − 1))((𝐵‘𝑘) · (𝑧↑𝑘)))) |
154 | | dvply1.g |
. . 3
⊢ (𝜑 → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(𝑁 − 1))((𝐵‘𝑘) · (𝑧↑𝑘)))) |
155 | 153, 154 | eqtr4d 2776 |
. 2
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))))) = 𝐺) |
156 | 2, 49, 155 | 3eqtrd 2777 |
1
⊢ (𝜑 → (ℂ D 𝐹) = 𝐺) |