Metamath Proof Explorer

Theorem dvply1

Description: Derivative of a polynomial, explicit sum version. (Contributed by Stefan O'Rear, 13-Nov-2014) (Revised by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypotheses dvply1.f ⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
dvply1.g ⊢ ( 𝜑 → 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
dvply1.a ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
dvply1.b ⊢ 𝐵 = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) )
dvply1.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion dvply1 ( 𝜑 → ( ℂ D 𝐹 ) = 𝐺 )

Proof

Step Hyp Ref Expression
1 dvply1.f ⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
2 dvply1.g ⊢ ( 𝜑 → 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
3 dvply1.a ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
4 dvply1.b ⊢ 𝐵 = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) )
5 dvply1.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
6 1 oveq2d ⊢ ( 𝜑 → ( ℂ D 𝐹 ) = ( ℂ D ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
7 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
8 7 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
9 8 toponrestid ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
10 cnelprrecn ⊢ ℂ ∈ { ℝ , ℂ }
11 10 a1i ⊢ ( 𝜑 → ℂ ∈ { ℝ , ℂ } )
12 7 cnfldtop ⊢ ( TopOpen ‘ ℂfld ) ∈ Top
13 unicntop ⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
14 13 topopn ⊢ ( ( TopOpen ‘ ℂfld ) ∈ Top → ℂ ∈ ( TopOpen ‘ ℂfld ) )
15 12 14 mp1i ⊢ ( 𝜑 → ℂ ∈ ( TopOpen ‘ ℂfld ) )
16 fzfid ⊢ ( 𝜑 → ( 0 ... 𝑁 ) ∈ Fin )
17 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
18 ffvelrn ⊢ ( ( 𝐴 : ℕ0 ⟶ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
19 3 17 18 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
20 19 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑧 ∈ ℂ ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
21 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑧 ∈ ℂ ) → 𝑧 ∈ ℂ )
22 17 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑧 ∈ ℂ ) → 𝑘 ∈ ℕ0 )
23 21 22 expcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑧 ∈ ℂ ) → ( 𝑧 ↑ 𝑘 ) ∈ ℂ )
24 20 23 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑧 ∈ ℂ ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ )
25 24 3impa ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ∈ ℂ ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ )
26 19 3adant3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ∈ ℂ ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
27 0cnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 = 0 ) → 0 ∈ ℂ )
28 simpl2 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ∈ ℂ ) ∧ ¬ 𝑘 = 0 ) → 𝑘 ∈ ( 0 ... 𝑁 ) )
29 28 17 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ∈ ℂ ) ∧ ¬ 𝑘 = 0 ) → 𝑘 ∈ ℕ0 )
30 29 nn0cnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ∈ ℂ ) ∧ ¬ 𝑘 = 0 ) → 𝑘 ∈ ℂ )
31 simpl3 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ∈ ℂ ) ∧ ¬ 𝑘 = 0 ) → 𝑧 ∈ ℂ )
32 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ∈ ℂ ) ∧ ¬ 𝑘 = 0 ) → ¬ 𝑘 = 0 )
33 elnn0 ⊢ ( 𝑘 ∈ ℕ0 ↔ ( 𝑘 ∈ ℕ ∨ 𝑘 = 0 ) )
34 29 33 sylib ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ∈ ℂ ) ∧ ¬ 𝑘 = 0 ) → ( 𝑘 ∈ ℕ ∨ 𝑘 = 0 ) )
35 orel2 ⊢ ( ¬ 𝑘 = 0 → ( ( 𝑘 ∈ ℕ ∨ 𝑘 = 0 ) → 𝑘 ∈ ℕ ) )
36 32 34 35 sylc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ∈ ℂ ) ∧ ¬ 𝑘 = 0 ) → 𝑘 ∈ ℕ )
37 nnm1nn0 ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 − 1 ) ∈ ℕ0 )
38 36 37 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ∈ ℂ ) ∧ ¬ 𝑘 = 0 ) → ( 𝑘 − 1 ) ∈ ℕ0 )
39 31 38 expcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ∈ ℂ ) ∧ ¬ 𝑘 = 0 ) → ( 𝑧 ↑ ( 𝑘 − 1 ) ) ∈ ℂ )
40 30 39 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ∈ ℂ ) ∧ ¬ 𝑘 = 0 ) → ( 𝑘 · ( 𝑧 ↑ ( 𝑘 − 1 ) ) ) ∈ ℂ )
41 27 40 ifclda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ∈ ℂ ) → if ( 𝑘 = 0 , 0 , ( 𝑘 · ( 𝑧 ↑ ( 𝑘 − 1 ) ) ) ) ∈ ℂ )
42 26 41 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑧 ∈ ℂ ) → ( ( 𝐴 ‘ 𝑘 ) · if ( 𝑘 = 0 , 0 , ( 𝑘 · ( 𝑧 ↑ ( 𝑘 − 1 ) ) ) ) ) ∈ ℂ )
43 10 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ℂ ∈ { ℝ , ℂ } )
44 c0ex ⊢ 0 ∈ V
45 ovex ⊢ ( 𝑘 · ( 𝑧 ↑ ( 𝑘 − 1 ) ) ) ∈ V
46 44 45 ifex ⊢ if ( 𝑘 = 0 , 0 , ( 𝑘 · ( 𝑧 ↑ ( 𝑘 − 1 ) ) ) ) ∈ V
47 46 a1i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑧 ∈ ℂ ) → if ( 𝑘 = 0 , 0 , ( 𝑘 · ( 𝑧 ↑ ( 𝑘 − 1 ) ) ) ) ∈ V )
48 17 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℕ0 )
49 dvexp2 ⊢ ( 𝑘 ∈ ℕ0 → ( ℂ D ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ if ( 𝑘 = 0 , 0 , ( 𝑘 · ( 𝑧 ↑ ( 𝑘 − 1 ) ) ) ) ) )
50 48 49 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ℂ D ( 𝑧 ∈ ℂ ↦ ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ if ( 𝑘 = 0 , 0 , ( 𝑘 · ( 𝑧 ↑ ( 𝑘 − 1 ) ) ) ) ) )
51 43 23 47 50 19 dvmptcmul ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ℂ D ( 𝑧 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) = ( 𝑧 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑘 ) · if ( 𝑘 = 0 , 0 , ( 𝑘 · ( 𝑧 ↑ ( 𝑘 − 1 ) ) ) ) ) ) )
52 9 7 11 15 16 25 42 51 dvmptfsum ⊢ ( 𝜑 → ( ℂ D ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · if ( 𝑘 = 0 , 0 , ( 𝑘 · ( 𝑧 ↑ ( 𝑘 − 1 ) ) ) ) ) ) )
53 elfznn ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℕ )
54 53 nnne0d ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ≠ 0 )
55 54 neneqd ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → ¬ 𝑘 = 0 )
56 55 adantl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ¬ 𝑘 = 0 )
57 56 iffalsed ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → if ( 𝑘 = 0 , 0 , ( 𝑘 · ( 𝑧 ↑ ( 𝑘 − 1 ) ) ) ) = ( 𝑘 · ( 𝑧 ↑ ( 𝑘 − 1 ) ) ) )
58 57 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐴 ‘ 𝑘 ) · if ( 𝑘 = 0 , 0 , ( 𝑘 · ( 𝑧 ↑ ( 𝑘 − 1 ) ) ) ) ) = ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 · ( 𝑧 ↑ ( 𝑘 − 1 ) ) ) ) )
59 58 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · if ( 𝑘 = 0 , 0 , ( 𝑘 · ( 𝑧 ↑ ( 𝑘 − 1 ) ) ) ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 · ( 𝑧 ↑ ( 𝑘 − 1 ) ) ) ) )
60 1eluzge0 ⊢ 1 ∈ ( ℤ≥ ‘ 0 )
61 fzss1 ⊢ ( 1 ∈ ( ℤ≥ ‘ 0 ) → ( 1 ... 𝑁 ) ⊆ ( 0 ... 𝑁 ) )
62 60 61 mp1i ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 1 ... 𝑁 ) ⊆ ( 0 ... 𝑁 ) )
63 3 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝐴 : ℕ0 ⟶ ℂ )
64 53 nnnn0d ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
65 63 64 18 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
66 54 adantl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ≠ 0 )
67 66 neneqd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ¬ 𝑘 = 0 )
68 67 iffalsed ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → if ( 𝑘 = 0 , 0 , ( 𝑘 · ( 𝑧 ↑ ( 𝑘 − 1 ) ) ) ) = ( 𝑘 · ( 𝑧 ↑ ( 𝑘 − 1 ) ) ) )
69 64 adantl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℕ0 )
70 69 nn0cnd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℂ )
71 simplr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑧 ∈ ℂ )
72 53 37 syl ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( 𝑘 − 1 ) ∈ ℕ0 )
73 72 adantl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑘 − 1 ) ∈ ℕ0 )
74 71 73 expcld ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑧 ↑ ( 𝑘 − 1 ) ) ∈ ℂ )
75 70 74 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑘 · ( 𝑧 ↑ ( 𝑘 − 1 ) ) ) ∈ ℂ )
76 68 75 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → if ( 𝑘 = 0 , 0 , ( 𝑘 · ( 𝑧 ↑ ( 𝑘 − 1 ) ) ) ) ∈ ℂ )
77 65 76 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐴 ‘ 𝑘 ) · if ( 𝑘 = 0 , 0 , ( 𝑘 · ( 𝑧 ↑ ( 𝑘 − 1 ) ) ) ) ) ∈ ℂ )
78 eldifn ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ ( 1 ... 𝑁 ) ) → ¬ 𝑘 ∈ ( 1 ... 𝑁 ) )
79 0p1e1 ⊢ ( 0 + 1 ) = 1
80 79 oveq1i ⊢ ( ( 0 + 1 ) ... 𝑁 ) = ( 1 ... 𝑁 )
81 80 eleq2i ⊢ ( 𝑘 ∈ ( ( 0 + 1 ) ... 𝑁 ) ↔ 𝑘 ∈ ( 1 ... 𝑁 ) )
82 78 81 sylnibr ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ ( 1 ... 𝑁 ) ) → ¬ 𝑘 ∈ ( ( 0 + 1 ) ... 𝑁 ) )
83 82 adantl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ ( 1 ... 𝑁 ) ) ) → ¬ 𝑘 ∈ ( ( 0 + 1 ) ... 𝑁 ) )
84 eldifi ⊢ ( 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ( 0 ... 𝑁 ) )
85 84 adantl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ ( 1 ... 𝑁 ) ) ) → 𝑘 ∈ ( 0 ... 𝑁 ) )
86 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
87 5 86 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
88 87 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ ( 1 ... 𝑁 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
89 elfzp12 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↔ ( 𝑘 = 0 ∨ 𝑘 ∈ ( ( 0 + 1 ) ... 𝑁 ) ) ) )
90 88 89 syl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ ( 1 ... 𝑁 ) ) ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↔ ( 𝑘 = 0 ∨ 𝑘 ∈ ( ( 0 + 1 ) ... 𝑁 ) ) ) )
91 85 90 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ ( 1 ... 𝑁 ) ) ) → ( 𝑘 = 0 ∨ 𝑘 ∈ ( ( 0 + 1 ) ... 𝑁 ) ) )
92 orel2 ⊢ ( ¬ 𝑘 ∈ ( ( 0 + 1 ) ... 𝑁 ) → ( ( 𝑘 = 0 ∨ 𝑘 ∈ ( ( 0 + 1 ) ... 𝑁 ) ) → 𝑘 = 0 ) )
93 83 91 92 sylc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ ( 1 ... 𝑁 ) ) ) → 𝑘 = 0 )
94 93 iftrued ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ ( 1 ... 𝑁 ) ) ) → if ( 𝑘 = 0 , 0 , ( 𝑘 · ( 𝑧 ↑ ( 𝑘 − 1 ) ) ) ) = 0 )
95 94 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ ( 1 ... 𝑁 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · if ( 𝑘 = 0 , 0 , ( 𝑘 · ( 𝑧 ↑ ( 𝑘 − 1 ) ) ) ) ) = ( ( 𝐴 ‘ 𝑘 ) · 0 ) )
96 63 17 18 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
97 96 mul01d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐴 ‘ 𝑘 ) · 0 ) = 0 )
98 84 97 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ ( 1 ... 𝑁 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · 0 ) = 0 )
99 95 98 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑁 ) ∖ ( 1 ... 𝑁 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · if ( 𝑘 = 0 , 0 , ( 𝑘 · ( 𝑧 ↑ ( 𝑘 − 1 ) ) ) ) ) = 0 )
100 fzfid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 0 ... 𝑁 ) ∈ Fin )
101 62 77 99 100 fsumss ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · if ( 𝑘 = 0 , 0 , ( 𝑘 · ( 𝑧 ↑ ( 𝑘 − 1 ) ) ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · if ( 𝑘 = 0 , 0 , ( 𝑘 · ( 𝑧 ↑ ( 𝑘 − 1 ) ) ) ) ) )
102 elfznn0 ⊢ ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑗 ∈ ℕ0 )
103 102 adantl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑗 ∈ ℕ0 )
104 103 nn0cnd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑗 ∈ ℂ )
105 ax-1cn ⊢ 1 ∈ ℂ
106 pncan ⊢ ( ( 𝑗 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑗 + 1 ) − 1 ) = 𝑗 )
107 104 105 106 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑗 + 1 ) − 1 ) = 𝑗 )
108 107 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑧 ↑ ( ( 𝑗 + 1 ) − 1 ) ) = ( 𝑧 ↑ 𝑗 ) )
109 108 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑗 + 1 ) · ( 𝑧 ↑ ( ( 𝑗 + 1 ) − 1 ) ) ) = ( ( 𝑗 + 1 ) · ( 𝑧 ↑ 𝑗 ) ) )
110 109 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝐴 ‘ ( 𝑗 + 1 ) ) · ( ( 𝑗 + 1 ) · ( 𝑧 ↑ ( ( 𝑗 + 1 ) − 1 ) ) ) ) = ( ( 𝐴 ‘ ( 𝑗 + 1 ) ) · ( ( 𝑗 + 1 ) · ( 𝑧 ↑ 𝑗 ) ) ) )
111 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝐴 : ℕ0 ⟶ ℂ )
112 peano2nn0 ⊢ ( 𝑗 ∈ ℕ0 → ( 𝑗 + 1 ) ∈ ℕ0 )
113 102 112 syl ⊢ ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑗 + 1 ) ∈ ℕ0 )
114 113 adantl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑗 + 1 ) ∈ ℕ0 )
115 111 114 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝐴 ‘ ( 𝑗 + 1 ) ) ∈ ℂ )
116 114 nn0cnd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑗 + 1 ) ∈ ℂ )
117 simplr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑧 ∈ ℂ )
118 117 103 expcld ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑧 ↑ 𝑗 ) ∈ ℂ )
119 115 116 118 mulassd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( 𝐴 ‘ ( 𝑗 + 1 ) ) · ( 𝑗 + 1 ) ) · ( 𝑧 ↑ 𝑗 ) ) = ( ( 𝐴 ‘ ( 𝑗 + 1 ) ) · ( ( 𝑗 + 1 ) · ( 𝑧 ↑ 𝑗 ) ) ) )
120 115 116 mulcomd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝐴 ‘ ( 𝑗 + 1 ) ) · ( 𝑗 + 1 ) ) = ( ( 𝑗 + 1 ) · ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) )
121 120 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( 𝐴 ‘ ( 𝑗 + 1 ) ) · ( 𝑗 + 1 ) ) · ( 𝑧 ↑ 𝑗 ) ) = ( ( ( 𝑗 + 1 ) · ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) · ( 𝑧 ↑ 𝑗 ) ) )
122 110 119 121 3eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝐴 ‘ ( 𝑗 + 1 ) ) · ( ( 𝑗 + 1 ) · ( 𝑧 ↑ ( ( 𝑗 + 1 ) − 1 ) ) ) ) = ( ( ( 𝑗 + 1 ) · ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) · ( 𝑧 ↑ 𝑗 ) ) )
123 122 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ‘ ( 𝑗 + 1 ) ) · ( ( 𝑗 + 1 ) · ( 𝑧 ↑ ( ( 𝑗 + 1 ) − 1 ) ) ) ) = Σ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( ( 𝑗 + 1 ) · ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) · ( 𝑧 ↑ 𝑗 ) ) )
124 1m1e0 ⊢ ( 1 − 1 ) = 0
125 124 oveq1i ⊢ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) = ( 0 ... ( 𝑁 − 1 ) )
126 125 sumeq1i ⊢ Σ 𝑗 ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ( ( 𝐴 ‘ ( 𝑗 + 1 ) ) · ( ( 𝑗 + 1 ) · ( 𝑧 ↑ ( ( 𝑗 + 1 ) − 1 ) ) ) ) = Σ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝐴 ‘ ( 𝑗 + 1 ) ) · ( ( 𝑗 + 1 ) · ( 𝑧 ↑ ( ( 𝑗 + 1 ) − 1 ) ) ) )
127 oveq1 ⊢ ( 𝑘 = 𝑗 → ( 𝑘 + 1 ) = ( 𝑗 + 1 ) )
128 fvoveq1 ⊢ ( 𝑘 = 𝑗 → ( 𝐴 ‘ ( 𝑘 + 1 ) ) = ( 𝐴 ‘ ( 𝑗 + 1 ) ) )
129 127 128 oveq12d ⊢ ( 𝑘 = 𝑗 → ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) = ( ( 𝑗 + 1 ) · ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) )
130 oveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝑧 ↑ 𝑘 ) = ( 𝑧 ↑ 𝑗 ) )
131 129 130 oveq12d ⊢ ( 𝑘 = 𝑗 → ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( ( 𝑗 + 1 ) · ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) · ( 𝑧 ↑ 𝑗 ) ) )
132 131 cbvsumv ⊢ Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( ( 𝑗 + 1 ) · ( 𝐴 ‘ ( 𝑗 + 1 ) ) ) · ( 𝑧 ↑ 𝑗 ) )
133 123 126 132 3eqtr4g ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑗 ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ( ( 𝐴 ‘ ( 𝑗 + 1 ) ) · ( ( 𝑗 + 1 ) · ( 𝑧 ↑ ( ( 𝑗 + 1 ) − 1 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑧 ↑ 𝑘 ) ) )
134 1zzd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 1 ∈ ℤ )
135 5 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝑁 ∈ ℕ0 )
136 135 nn0zd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝑁 ∈ ℤ )
137 65 75 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 · ( 𝑧 ↑ ( 𝑘 − 1 ) ) ) ) ∈ ℂ )
138 fveq2 ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ ( 𝑗 + 1 ) ) )
139 id ⊢ ( 𝑘 = ( 𝑗 + 1 ) → 𝑘 = ( 𝑗 + 1 ) )
140 oveq1 ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( 𝑘 − 1 ) = ( ( 𝑗 + 1 ) − 1 ) )
141 140 oveq2d ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( 𝑧 ↑ ( 𝑘 − 1 ) ) = ( 𝑧 ↑ ( ( 𝑗 + 1 ) − 1 ) ) )
142 139 141 oveq12d ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( 𝑘 · ( 𝑧 ↑ ( 𝑘 − 1 ) ) ) = ( ( 𝑗 + 1 ) · ( 𝑧 ↑ ( ( 𝑗 + 1 ) − 1 ) ) ) )
143 138 142 oveq12d ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 · ( 𝑧 ↑ ( 𝑘 − 1 ) ) ) ) = ( ( 𝐴 ‘ ( 𝑗 + 1 ) ) · ( ( 𝑗 + 1 ) · ( 𝑧 ↑ ( ( 𝑗 + 1 ) − 1 ) ) ) ) )
144 134 134 136 137 143 fsumshftm ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 · ( 𝑧 ↑ ( 𝑘 − 1 ) ) ) ) = Σ 𝑗 ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ( ( 𝐴 ‘ ( 𝑗 + 1 ) ) · ( ( 𝑗 + 1 ) · ( 𝑧 ↑ ( ( 𝑗 + 1 ) − 1 ) ) ) ) )
145 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ℕ0 )
146 145 adantl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ℕ0 )
147 ovex ⊢ ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) ∈ V
148 4 fvmpt2 ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) ∈ V ) → ( 𝐵 ‘ 𝑘 ) = ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) )
149 146 147 148 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝐵 ‘ 𝑘 ) = ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) )
150 149 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑧 ↑ 𝑘 ) ) )
151 150 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( ( 𝑘 + 1 ) · ( 𝐴 ‘ ( 𝑘 + 1 ) ) ) · ( 𝑧 ↑ 𝑘 ) ) )
152 133 144 151 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 · ( 𝑧 ↑ ( 𝑘 − 1 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
153 59 101 152 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · if ( 𝑘 = 0 , 0 , ( 𝑘 · ( 𝑧 ↑ ( 𝑘 − 1 ) ) ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
154 153 mpteq2dva ⊢ ( 𝜑 → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · if ( 𝑘 = 0 , 0 , ( 𝑘 · ( 𝑧 ↑ ( 𝑘 − 1 ) ) ) ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
155 154 2 eqtr4d ⊢ ( 𝜑 → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · if ( 𝑘 = 0 , 0 , ( 𝑘 · ( 𝑧 ↑ ( 𝑘 − 1 ) ) ) ) ) ) = 𝐺 )
156 6 52 155 3eqtrd ⊢ ( 𝜑 → ( ℂ D 𝐹 ) = 𝐺 )