MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dvply1 Structured version   Visualization version   GIF version

Theorem dvply1 24344
Description: Derivative of a polynomial, explicit sum version. (Contributed by Stefan O'Rear, 13-Nov-2014.) (Revised by Mario Carneiro, 11-Feb-2015.)
Hypotheses
Ref Expression
dvply1.f (𝜑𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑧𝑘))))
dvply1.g (𝜑𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(𝑁 − 1))((𝐵𝑘) · (𝑧𝑘))))
dvply1.a (𝜑𝐴:ℕ0⟶ℂ)
dvply1.b 𝐵 = (𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) · (𝐴‘(𝑘 + 1))))
dvply1.n (𝜑𝑁 ∈ ℕ0)
Assertion
Ref Expression
dvply1 (𝜑 → (ℂ D 𝐹) = 𝐺)
Distinct variable groups:   𝜑,𝑧,𝑘   𝑧,𝐴,𝑘   𝑧,𝐵   𝑘,𝑁,𝑧
Allowed substitution hints:   𝐵(𝑘)   𝐹(𝑧,𝑘)   𝐺(𝑧,𝑘)

Proof of Theorem dvply1
Dummy variable 𝑗 is distinct from all other variables.
StepHypRef Expression
1 dvply1.f . . 3 (𝜑𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑧𝑘))))
21oveq2d 6862 . 2 (𝜑 → (ℂ D 𝐹) = (ℂ D (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑧𝑘)))))
3 eqid 2765 . . . . 5 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
43cnfldtopon 22879 . . . 4 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
54toponrestid 21019 . . 3 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
6 cnelprrecn 10286 . . . 4 ℂ ∈ {ℝ, ℂ}
76a1i 11 . . 3 (𝜑 → ℂ ∈ {ℝ, ℂ})
83cnfldtop 22880 . . . 4 (TopOpen‘ℂfld) ∈ Top
94toponunii 21014 . . . . 5 ℂ = (TopOpen‘ℂfld)
109topopn 21004 . . . 4 ((TopOpen‘ℂfld) ∈ Top → ℂ ∈ (TopOpen‘ℂfld))
118, 10mp1i 13 . . 3 (𝜑 → ℂ ∈ (TopOpen‘ℂfld))
12 fzfid 12985 . . 3 (𝜑 → (0...𝑁) ∈ Fin)
13 dvply1.a . . . . . . 7 (𝜑𝐴:ℕ0⟶ℂ)
14 elfznn0 12645 . . . . . . 7 (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
15 ffvelrn 6551 . . . . . . 7 ((𝐴:ℕ0⟶ℂ ∧ 𝑘 ∈ ℕ0) → (𝐴𝑘) ∈ ℂ)
1613, 14, 15syl2an 589 . . . . . 6 ((𝜑𝑘 ∈ (0...𝑁)) → (𝐴𝑘) ∈ ℂ)
1716adantr 472 . . . . 5 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑧 ∈ ℂ) → (𝐴𝑘) ∈ ℂ)
18 simpr 477 . . . . . 6 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑧 ∈ ℂ) → 𝑧 ∈ ℂ)
1914ad2antlr 718 . . . . . 6 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑧 ∈ ℂ) → 𝑘 ∈ ℕ0)
2018, 19expcld 13220 . . . . 5 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑧 ∈ ℂ) → (𝑧𝑘) ∈ ℂ)
2117, 20mulcld 10318 . . . 4 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑧 ∈ ℂ) → ((𝐴𝑘) · (𝑧𝑘)) ∈ ℂ)
22213impa 1136 . . 3 ((𝜑𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) → ((𝐴𝑘) · (𝑧𝑘)) ∈ ℂ)
23163adant3 1162 . . . 4 ((𝜑𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) → (𝐴𝑘) ∈ ℂ)
24 0cnd 10290 . . . . 5 (((𝜑𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 = 0) → 0 ∈ ℂ)
25 simpl2 1244 . . . . . . . 8 (((𝜑𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → 𝑘 ∈ (0...𝑁))
2625, 14syl 17 . . . . . . 7 (((𝜑𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → 𝑘 ∈ ℕ0)
2726nn0cnd 11604 . . . . . 6 (((𝜑𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → 𝑘 ∈ ℂ)
28 simpl3 1246 . . . . . . 7 (((𝜑𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → 𝑧 ∈ ℂ)
29 simpr 477 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → ¬ 𝑘 = 0)
30 elnn0 11544 . . . . . . . . . 10 (𝑘 ∈ ℕ0 ↔ (𝑘 ∈ ℕ ∨ 𝑘 = 0))
3126, 30sylib 209 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → (𝑘 ∈ ℕ ∨ 𝑘 = 0))
32 orel2 914 . . . . . . . . 9 𝑘 = 0 → ((𝑘 ∈ ℕ ∨ 𝑘 = 0) → 𝑘 ∈ ℕ))
3329, 31, 32sylc 65 . . . . . . . 8 (((𝜑𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → 𝑘 ∈ ℕ)
34 nnm1nn0 11585 . . . . . . . 8 (𝑘 ∈ ℕ → (𝑘 − 1) ∈ ℕ0)
3533, 34syl 17 . . . . . . 7 (((𝜑𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → (𝑘 − 1) ∈ ℕ0)
3628, 35expcld 13220 . . . . . 6 (((𝜑𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → (𝑧↑(𝑘 − 1)) ∈ ℂ)
3727, 36mulcld 10318 . . . . 5 (((𝜑𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) ∧ ¬ 𝑘 = 0) → (𝑘 · (𝑧↑(𝑘 − 1))) ∈ ℂ)
3824, 37ifclda 4279 . . . 4 ((𝜑𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) → if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))) ∈ ℂ)
3923, 38mulcld 10318 . . 3 ((𝜑𝑘 ∈ (0...𝑁) ∧ 𝑧 ∈ ℂ) → ((𝐴𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))) ∈ ℂ)
406a1i 11 . . . 4 ((𝜑𝑘 ∈ (0...𝑁)) → ℂ ∈ {ℝ, ℂ})
41 c0ex 10291 . . . . . 6 0 ∈ V
42 ovex 6878 . . . . . 6 (𝑘 · (𝑧↑(𝑘 − 1))) ∈ V
4341, 42ifex 4293 . . . . 5 if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))) ∈ V
4443a1i 11 . . . 4 (((𝜑𝑘 ∈ (0...𝑁)) ∧ 𝑧 ∈ ℂ) → if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))) ∈ V)
4514adantl 473 . . . . 5 ((𝜑𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
46 dvexp2 24022 . . . . 5 (𝑘 ∈ ℕ0 → (ℂ D (𝑧 ∈ ℂ ↦ (𝑧𝑘))) = (𝑧 ∈ ℂ ↦ if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))))
4745, 46syl 17 . . . 4 ((𝜑𝑘 ∈ (0...𝑁)) → (ℂ D (𝑧 ∈ ℂ ↦ (𝑧𝑘))) = (𝑧 ∈ ℂ ↦ if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))))
4840, 20, 44, 47, 16dvmptcmul 24032 . . 3 ((𝜑𝑘 ∈ (0...𝑁)) → (ℂ D (𝑧 ∈ ℂ ↦ ((𝐴𝑘) · (𝑧𝑘)))) = (𝑧 ∈ ℂ ↦ ((𝐴𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))))))
495, 3, 7, 11, 12, 22, 39, 48dvmptfsum 24043 . 2 (𝜑 → (ℂ D (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · (𝑧𝑘)))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))))))
50 elfznn 12582 . . . . . . . . . . 11 (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℕ)
5150nnne0d 11326 . . . . . . . . . 10 (𝑘 ∈ (1...𝑁) → 𝑘 ≠ 0)
5251neneqd 2942 . . . . . . . . 9 (𝑘 ∈ (1...𝑁) → ¬ 𝑘 = 0)
5352adantl 473 . . . . . . . 8 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → ¬ 𝑘 = 0)
5453iffalsed 4256 . . . . . . 7 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))) = (𝑘 · (𝑧↑(𝑘 − 1))))
5554oveq2d 6862 . . . . . 6 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → ((𝐴𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))) = ((𝐴𝑘) · (𝑘 · (𝑧↑(𝑘 − 1)))))
5655sumeq2dv 14732 . . . . 5 ((𝜑𝑧 ∈ ℂ) → Σ𝑘 ∈ (1...𝑁)((𝐴𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))) = Σ𝑘 ∈ (1...𝑁)((𝐴𝑘) · (𝑘 · (𝑧↑(𝑘 − 1)))))
57 1eluzge0 11937 . . . . . . 7 1 ∈ (ℤ‘0)
58 fzss1 12592 . . . . . . 7 (1 ∈ (ℤ‘0) → (1...𝑁) ⊆ (0...𝑁))
5957, 58mp1i 13 . . . . . 6 ((𝜑𝑧 ∈ ℂ) → (1...𝑁) ⊆ (0...𝑁))
6013adantr 472 . . . . . . . 8 ((𝜑𝑧 ∈ ℂ) → 𝐴:ℕ0⟶ℂ)
6150nnnn0d 11602 . . . . . . . 8 (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℕ0)
6260, 61, 15syl2an 589 . . . . . . 7 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → (𝐴𝑘) ∈ ℂ)
6351adantl 473 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → 𝑘 ≠ 0)
6463neneqd 2942 . . . . . . . . 9 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → ¬ 𝑘 = 0)
6564iffalsed 4256 . . . . . . . 8 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))) = (𝑘 · (𝑧↑(𝑘 − 1))))
6661adantl 473 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → 𝑘 ∈ ℕ0)
6766nn0cnd 11604 . . . . . . . . 9 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → 𝑘 ∈ ℂ)
68 simplr 785 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → 𝑧 ∈ ℂ)
6950, 34syl 17 . . . . . . . . . . 11 (𝑘 ∈ (1...𝑁) → (𝑘 − 1) ∈ ℕ0)
7069adantl 473 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → (𝑘 − 1) ∈ ℕ0)
7168, 70expcld 13220 . . . . . . . . 9 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → (𝑧↑(𝑘 − 1)) ∈ ℂ)
7267, 71mulcld 10318 . . . . . . . 8 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → (𝑘 · (𝑧↑(𝑘 − 1))) ∈ ℂ)
7365, 72eqeltrd 2844 . . . . . . 7 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))) ∈ ℂ)
7462, 73mulcld 10318 . . . . . 6 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → ((𝐴𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))) ∈ ℂ)
75 eldifn 3897 . . . . . . . . . . . 12 (𝑘 ∈ ((0...𝑁) ∖ (1...𝑁)) → ¬ 𝑘 ∈ (1...𝑁))
76 0p1e1 11405 . . . . . . . . . . . . . 14 (0 + 1) = 1
7776oveq1i 6856 . . . . . . . . . . . . 13 ((0 + 1)...𝑁) = (1...𝑁)
7877eleq2i 2836 . . . . . . . . . . . 12 (𝑘 ∈ ((0 + 1)...𝑁) ↔ 𝑘 ∈ (1...𝑁))
7975, 78sylnibr 320 . . . . . . . . . . 11 (𝑘 ∈ ((0...𝑁) ∖ (1...𝑁)) → ¬ 𝑘 ∈ ((0 + 1)...𝑁))
8079adantl 473 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → ¬ 𝑘 ∈ ((0 + 1)...𝑁))
81 eldifi 3896 . . . . . . . . . . . 12 (𝑘 ∈ ((0...𝑁) ∖ (1...𝑁)) → 𝑘 ∈ (0...𝑁))
8281adantl 473 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → 𝑘 ∈ (0...𝑁))
83 dvply1.n . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℕ0)
84 nn0uz 11927 . . . . . . . . . . . . . 14 0 = (ℤ‘0)
8583, 84syl6eleq 2854 . . . . . . . . . . . . 13 (𝜑𝑁 ∈ (ℤ‘0))
8685ad2antrr 717 . . . . . . . . . . . 12 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → 𝑁 ∈ (ℤ‘0))
87 elfzp12 12631 . . . . . . . . . . . 12 (𝑁 ∈ (ℤ‘0) → (𝑘 ∈ (0...𝑁) ↔ (𝑘 = 0 ∨ 𝑘 ∈ ((0 + 1)...𝑁))))
8886, 87syl 17 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → (𝑘 ∈ (0...𝑁) ↔ (𝑘 = 0 ∨ 𝑘 ∈ ((0 + 1)...𝑁))))
8982, 88mpbid 223 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → (𝑘 = 0 ∨ 𝑘 ∈ ((0 + 1)...𝑁)))
90 orel2 914 . . . . . . . . . 10 𝑘 ∈ ((0 + 1)...𝑁) → ((𝑘 = 0 ∨ 𝑘 ∈ ((0 + 1)...𝑁)) → 𝑘 = 0))
9180, 89, 90sylc 65 . . . . . . . . 9 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → 𝑘 = 0)
9291iftrued 4253 . . . . . . . 8 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))) = 0)
9392oveq2d 6862 . . . . . . 7 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → ((𝐴𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))) = ((𝐴𝑘) · 0))
9460, 14, 15syl2an 589 . . . . . . . . 9 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → (𝐴𝑘) ∈ ℂ)
9594mul01d 10493 . . . . . . . 8 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴𝑘) · 0) = 0)
9681, 95sylan2 586 . . . . . . 7 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → ((𝐴𝑘) · 0) = 0)
9793, 96eqtrd 2799 . . . . . 6 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...𝑁) ∖ (1...𝑁))) → ((𝐴𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))) = 0)
98 fzfid 12985 . . . . . 6 ((𝜑𝑧 ∈ ℂ) → (0...𝑁) ∈ Fin)
9959, 74, 97, 98fsumss 14755 . . . . 5 ((𝜑𝑧 ∈ ℂ) → Σ𝑘 ∈ (1...𝑁)((𝐴𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))) = Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))))
100 elfznn0 12645 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 ∈ ℕ0)
101100adantl 473 . . . . . . . . . . . . . 14 (((𝜑𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑗 ∈ ℕ0)
102101nn0cnd 11604 . . . . . . . . . . . . 13 (((𝜑𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑗 ∈ ℂ)
103 ax-1cn 10251 . . . . . . . . . . . . 13 1 ∈ ℂ
104 pncan 10545 . . . . . . . . . . . . 13 ((𝑗 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑗 + 1) − 1) = 𝑗)
105102, 103, 104sylancl 580 . . . . . . . . . . . 12 (((𝜑𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑗 + 1) − 1) = 𝑗)
106105oveq2d 6862 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑧↑((𝑗 + 1) − 1)) = (𝑧𝑗))
107106oveq2d 6862 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1))) = ((𝑗 + 1) · (𝑧𝑗)))
108107oveq2d 6862 . . . . . . . . 9 (((𝜑𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1)))) = ((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧𝑗))))
10913ad2antrr 717 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝐴:ℕ0⟶ℂ)
110 peano2nn0 11584 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ0 → (𝑗 + 1) ∈ ℕ0)
111100, 110syl 17 . . . . . . . . . . . 12 (𝑗 ∈ (0...(𝑁 − 1)) → (𝑗 + 1) ∈ ℕ0)
112111adantl 473 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑗 + 1) ∈ ℕ0)
113109, 112ffvelrnd 6554 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝐴‘(𝑗 + 1)) ∈ ℂ)
114112nn0cnd 11604 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑗 + 1) ∈ ℂ)
115 simplr 785 . . . . . . . . . . 11 (((𝜑𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑧 ∈ ℂ)
116115, 101expcld 13220 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑧𝑗) ∈ ℂ)
117113, 114, 116mulassd 10321 . . . . . . . . 9 (((𝜑𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (((𝐴‘(𝑗 + 1)) · (𝑗 + 1)) · (𝑧𝑗)) = ((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧𝑗))))
118113, 114mulcomd 10319 . . . . . . . . . 10 (((𝜑𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝐴‘(𝑗 + 1)) · (𝑗 + 1)) = ((𝑗 + 1) · (𝐴‘(𝑗 + 1))))
119118oveq1d 6861 . . . . . . . . 9 (((𝜑𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (((𝐴‘(𝑗 + 1)) · (𝑗 + 1)) · (𝑧𝑗)) = (((𝑗 + 1) · (𝐴‘(𝑗 + 1))) · (𝑧𝑗)))
120108, 117, 1193eqtr2d 2805 . . . . . . . 8 (((𝜑𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1)))) = (((𝑗 + 1) · (𝐴‘(𝑗 + 1))) · (𝑧𝑗)))
121120sumeq2dv 14732 . . . . . . 7 ((𝜑𝑧 ∈ ℂ) → Σ𝑗 ∈ (0...(𝑁 − 1))((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1)))) = Σ𝑗 ∈ (0...(𝑁 − 1))(((𝑗 + 1) · (𝐴‘(𝑗 + 1))) · (𝑧𝑗)))
122 1m1e0 11348 . . . . . . . . 9 (1 − 1) = 0
123122oveq1i 6856 . . . . . . . 8 ((1 − 1)...(𝑁 − 1)) = (0...(𝑁 − 1))
124123sumeq1i 14727 . . . . . . 7 Σ𝑗 ∈ ((1 − 1)...(𝑁 − 1))((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1)))) = Σ𝑗 ∈ (0...(𝑁 − 1))((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1))))
125 oveq1 6853 . . . . . . . . . 10 (𝑘 = 𝑗 → (𝑘 + 1) = (𝑗 + 1))
126 fvoveq1 6869 . . . . . . . . . 10 (𝑘 = 𝑗 → (𝐴‘(𝑘 + 1)) = (𝐴‘(𝑗 + 1)))
127125, 126oveq12d 6864 . . . . . . . . 9 (𝑘 = 𝑗 → ((𝑘 + 1) · (𝐴‘(𝑘 + 1))) = ((𝑗 + 1) · (𝐴‘(𝑗 + 1))))
128 oveq2 6854 . . . . . . . . 9 (𝑘 = 𝑗 → (𝑧𝑘) = (𝑧𝑗))
129127, 128oveq12d 6864 . . . . . . . 8 (𝑘 = 𝑗 → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑧𝑘)) = (((𝑗 + 1) · (𝐴‘(𝑗 + 1))) · (𝑧𝑗)))
130129cbvsumv 14725 . . . . . . 7 Σ𝑘 ∈ (0...(𝑁 − 1))(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑧𝑘)) = Σ𝑗 ∈ (0...(𝑁 − 1))(((𝑗 + 1) · (𝐴‘(𝑗 + 1))) · (𝑧𝑗))
131121, 124, 1303eqtr4g 2824 . . . . . 6 ((𝜑𝑧 ∈ ℂ) → Σ𝑗 ∈ ((1 − 1)...(𝑁 − 1))((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1)))) = Σ𝑘 ∈ (0...(𝑁 − 1))(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑧𝑘)))
132 1zzd 11660 . . . . . . 7 ((𝜑𝑧 ∈ ℂ) → 1 ∈ ℤ)
13383adantr 472 . . . . . . . 8 ((𝜑𝑧 ∈ ℂ) → 𝑁 ∈ ℕ0)
134133nn0zd 11732 . . . . . . 7 ((𝜑𝑧 ∈ ℂ) → 𝑁 ∈ ℤ)
13562, 72mulcld 10318 . . . . . . 7 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → ((𝐴𝑘) · (𝑘 · (𝑧↑(𝑘 − 1)))) ∈ ℂ)
136 fveq2 6379 . . . . . . . 8 (𝑘 = (𝑗 + 1) → (𝐴𝑘) = (𝐴‘(𝑗 + 1)))
137 id 22 . . . . . . . . 9 (𝑘 = (𝑗 + 1) → 𝑘 = (𝑗 + 1))
138 oveq1 6853 . . . . . . . . . 10 (𝑘 = (𝑗 + 1) → (𝑘 − 1) = ((𝑗 + 1) − 1))
139138oveq2d 6862 . . . . . . . . 9 (𝑘 = (𝑗 + 1) → (𝑧↑(𝑘 − 1)) = (𝑧↑((𝑗 + 1) − 1)))
140137, 139oveq12d 6864 . . . . . . . 8 (𝑘 = (𝑗 + 1) → (𝑘 · (𝑧↑(𝑘 − 1))) = ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1))))
141136, 140oveq12d 6864 . . . . . . 7 (𝑘 = (𝑗 + 1) → ((𝐴𝑘) · (𝑘 · (𝑧↑(𝑘 − 1)))) = ((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1)))))
142132, 132, 134, 135, 141fsumshftm 14811 . . . . . 6 ((𝜑𝑧 ∈ ℂ) → Σ𝑘 ∈ (1...𝑁)((𝐴𝑘) · (𝑘 · (𝑧↑(𝑘 − 1)))) = Σ𝑗 ∈ ((1 − 1)...(𝑁 − 1))((𝐴‘(𝑗 + 1)) · ((𝑗 + 1) · (𝑧↑((𝑗 + 1) − 1)))))
143 elfznn0 12645 . . . . . . . . . 10 (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ0)
144143adantl 473 . . . . . . . . 9 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ ℕ0)
145 ovex 6878 . . . . . . . . 9 ((𝑘 + 1) · (𝐴‘(𝑘 + 1))) ∈ V
146 dvply1.b . . . . . . . . . 10 𝐵 = (𝑘 ∈ ℕ0 ↦ ((𝑘 + 1) · (𝐴‘(𝑘 + 1))))
147146fvmpt2 6484 . . . . . . . . 9 ((𝑘 ∈ ℕ0 ∧ ((𝑘 + 1) · (𝐴‘(𝑘 + 1))) ∈ V) → (𝐵𝑘) = ((𝑘 + 1) · (𝐴‘(𝑘 + 1))))
148144, 145, 147sylancl 580 . . . . . . . 8 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐵𝑘) = ((𝑘 + 1) · (𝐴‘(𝑘 + 1))))
149148oveq1d 6861 . . . . . . 7 (((𝜑𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝐵𝑘) · (𝑧𝑘)) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑧𝑘)))
150149sumeq2dv 14732 . . . . . 6 ((𝜑𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...(𝑁 − 1))((𝐵𝑘) · (𝑧𝑘)) = Σ𝑘 ∈ (0...(𝑁 − 1))(((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑧𝑘)))
151131, 142, 1503eqtr4d 2809 . . . . 5 ((𝜑𝑧 ∈ ℂ) → Σ𝑘 ∈ (1...𝑁)((𝐴𝑘) · (𝑘 · (𝑧↑(𝑘 − 1)))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝐵𝑘) · (𝑧𝑘)))
15256, 99, 1513eqtr3d 2807 . . . 4 ((𝜑𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1))))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝐵𝑘) · (𝑧𝑘)))
153152mpteq2dva 4905 . . 3 (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(𝑁 − 1))((𝐵𝑘) · (𝑧𝑘))))
154 dvply1.g . . 3 (𝜑𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(𝑁 − 1))((𝐵𝑘) · (𝑧𝑘))))
155153, 154eqtr4d 2802 . 2 (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴𝑘) · if(𝑘 = 0, 0, (𝑘 · (𝑧↑(𝑘 − 1)))))) = 𝐺)
1562, 49, 1553eqtrd 2803 1 (𝜑 → (ℂ D 𝐹) = 𝐺)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 873  w3a 1107   = wceq 1652  wcel 2155  wne 2937  Vcvv 3350  cdif 3731  wss 3734  ifcif 4245  {cpr 4338  cmpt 4890  wf 6066  cfv 6070  (class class class)co 6846  cc 10191  cr 10192  0cc0 10193  1c1 10194   + caddc 10196   · cmul 10198  cmin 10524  cn 11278  0cn0 11542  cuz 11891  ...cfz 12538  cexp 13072  Σcsu 14715  TopOpenctopn 16362  fldccnfld 20033  Topctop 20991   D cdv 23932
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7151  ax-inf2 8757  ax-cnex 10249  ax-resscn 10250  ax-1cn 10251  ax-icn 10252  ax-addcl 10253  ax-addrcl 10254  ax-mulcl 10255  ax-mulrcl 10256  ax-mulcom 10257  ax-addass 10258  ax-mulass 10259  ax-distr 10260  ax-i2m1 10261  ax-1ne0 10262  ax-1rid 10263  ax-rnegex 10264  ax-rrecex 10265  ax-cnre 10266  ax-pre-lttri 10267  ax-pre-lttrn 10268  ax-pre-ltadd 10269  ax-pre-mulgt0 10270  ax-pre-sup 10271  ax-addf 10272  ax-mulf 10273
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-int 4636  df-iun 4680  df-iin 4681  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-se 5239  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-isom 6079  df-riota 6807  df-ov 6849  df-oprab 6850  df-mpt2 6851  df-of 7099  df-om 7268  df-1st 7370  df-2nd 7371  df-supp 7502  df-wrecs 7614  df-recs 7676  df-rdg 7714  df-1o 7768  df-2o 7769  df-oadd 7772  df-er 7951  df-map 8066  df-pm 8067  df-ixp 8118  df-en 8165  df-dom 8166  df-sdom 8167  df-fin 8168  df-fsupp 8487  df-fi 8528  df-sup 8559  df-inf 8560  df-oi 8626  df-card 9020  df-cda 9247  df-pnf 10334  df-mnf 10335  df-xr 10336  df-ltxr 10337  df-le 10338  df-sub 10526  df-neg 10527  df-div 10943  df-nn 11279  df-2 11339  df-3 11340  df-4 11341  df-5 11342  df-6 11343  df-7 11344  df-8 11345  df-9 11346  df-n0 11543  df-z 11629  df-dec 11746  df-uz 11892  df-q 11995  df-rp 12034  df-xneg 12151  df-xadd 12152  df-xmul 12153  df-icc 12389  df-fz 12539  df-fzo 12679  df-seq 13014  df-exp 13073  df-hash 13327  df-cj 14138  df-re 14139  df-im 14140  df-sqrt 14274  df-abs 14275  df-clim 14518  df-sum 14716  df-struct 16146  df-ndx 16147  df-slot 16148  df-base 16150  df-sets 16151  df-ress 16152  df-plusg 16241  df-mulr 16242  df-starv 16243  df-sca 16244  df-vsca 16245  df-ip 16246  df-tset 16247  df-ple 16248  df-ds 16250  df-unif 16251  df-hom 16252  df-cco 16253  df-rest 16363  df-topn 16364  df-0g 16382  df-gsum 16383  df-topgen 16384  df-pt 16385  df-prds 16388  df-xrs 16442  df-qtop 16447  df-imas 16448  df-xps 16450  df-mre 16526  df-mrc 16527  df-acs 16529  df-mgm 17522  df-sgrp 17564  df-mnd 17575  df-submnd 17616  df-mulg 17822  df-cntz 18027  df-cmn 18475  df-psmet 20025  df-xmet 20026  df-met 20027  df-bl 20028  df-mopn 20029  df-fbas 20030  df-fg 20031  df-cnfld 20034  df-top 20992  df-topon 21009  df-topsp 21031  df-bases 21044  df-cld 21117  df-ntr 21118  df-cls 21119  df-nei 21196  df-lp 21234  df-perf 21235  df-cn 21325  df-cnp 21326  df-haus 21413  df-tx 21659  df-hmeo 21852  df-fil 21943  df-fm 22035  df-flim 22036  df-flf 22037  df-xms 22418  df-ms 22419  df-tms 22420  df-cncf 22974  df-limc 23935  df-dv 23936
This theorem is referenced by:  dvply2g  24345
  Copyright terms: Public domain W3C validator