This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) )
dvply1.g 
|- ( ph -> G = ( z e. CC |-> sum_ k e. ( 0 ... ( N - 1 ) ) ( ( B ` k ) x. ( z ^ k ) ) ) )
dvply1.a 
|- ( ph -> A : NN0 --> CC )
dvply1.b 
|- B = ( k e. NN0 |-> ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) )
dvply1.n 
|- ( ph -> N e. NN0 )
Assertion dvply1 
|- ( ph -> ( CC _D F ) = G )

Proof

Step Hyp Ref Expression
1 dvply1.f 
 |-  ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) )
2 dvply1.g 
 |-  ( ph -> G = ( z e. CC |-> sum_ k e. ( 0 ... ( N - 1 ) ) ( ( B ` k ) x. ( z ^ k ) ) ) )
3 dvply1.a 
 |-  ( ph -> A : NN0 --> CC )
4 dvply1.b 
 |-  B = ( k e. NN0 |-> ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) )
5 dvply1.n 
 |-  ( ph -> N e. NN0 )
6 1 oveq2d 
 |-  ( ph -> ( CC _D F ) = ( CC _D ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) ) )
7 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
8 7 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
9 8 toponrestid 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
10 cnelprrecn 
 |-  CC e. { RR , CC }
11 10 a1i 
 |-  ( ph -> CC e. { RR , CC } )
12 7 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
13 unicntop 
 |-  CC = U. ( TopOpen ` CCfld )
14 13 topopn 
 |-  ( ( TopOpen ` CCfld ) e. Top -> CC e. ( TopOpen ` CCfld ) )
15 12 14 mp1i 
 |-  ( ph -> CC e. ( TopOpen ` CCfld ) )
16 fzfid 
 |-  ( ph -> ( 0 ... N ) e. Fin )
17 elfznn0 
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
18 ffvelcdm 
 |-  ( ( A : NN0 --> CC /\ k e. NN0 ) -> ( A ` k ) e. CC )
19 3 17 18 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( A ` k ) e. CC )
20 19 adantr 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ z e. CC ) -> ( A ` k ) e. CC )
21 simpr 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ z e. CC ) -> z e. CC )
22 17 ad2antlr 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ z e. CC ) -> k e. NN0 )
23 21 22 expcld 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ z e. CC ) -> ( z ^ k ) e. CC )
24 20 23 mulcld 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ z e. CC ) -> ( ( A ` k ) x. ( z ^ k ) ) e. CC )
25 24 3impa 
 |-  ( ( ph /\ k e. ( 0 ... N ) /\ z e. CC ) -> ( ( A ` k ) x. ( z ^ k ) ) e. CC )
26 19 3adant3 
 |-  ( ( ph /\ k e. ( 0 ... N ) /\ z e. CC ) -> ( A ` k ) e. CC )
27 0cnd 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) /\ z e. CC ) /\ k = 0 ) -> 0 e. CC )
28 simpl2 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) /\ z e. CC ) /\ -. k = 0 ) -> k e. ( 0 ... N ) )
29 28 17 syl 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) /\ z e. CC ) /\ -. k = 0 ) -> k e. NN0 )
30 29 nn0cnd 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) /\ z e. CC ) /\ -. k = 0 ) -> k e. CC )
31 simpl3 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) /\ z e. CC ) /\ -. k = 0 ) -> z e. CC )
32 simpr 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) /\ z e. CC ) /\ -. k = 0 ) -> -. k = 0 )
33 elnn0 
 |-  ( k e. NN0 <-> ( k e. NN \/ k = 0 ) )
34 29 33 sylib 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) /\ z e. CC ) /\ -. k = 0 ) -> ( k e. NN \/ k = 0 ) )
35 orel2 
 |-  ( -. k = 0 -> ( ( k e. NN \/ k = 0 ) -> k e. NN ) )
36 32 34 35 sylc 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) /\ z e. CC ) /\ -. k = 0 ) -> k e. NN )
37 nnm1nn0 
 |-  ( k e. NN -> ( k - 1 ) e. NN0 )
38 36 37 syl 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) /\ z e. CC ) /\ -. k = 0 ) -> ( k - 1 ) e. NN0 )
39 31 38 expcld 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) /\ z e. CC ) /\ -. k = 0 ) -> ( z ^ ( k - 1 ) ) e. CC )
40 30 39 mulcld 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) /\ z e. CC ) /\ -. k = 0 ) -> ( k x. ( z ^ ( k - 1 ) ) ) e. CC )
41 27 40 ifclda 
 |-  ( ( ph /\ k e. ( 0 ... N ) /\ z e. CC ) -> if ( k = 0 , 0 , ( k x. ( z ^ ( k - 1 ) ) ) ) e. CC )
42 26 41 mulcld 
 |-  ( ( ph /\ k e. ( 0 ... N ) /\ z e. CC ) -> ( ( A ` k ) x. if ( k = 0 , 0 , ( k x. ( z ^ ( k - 1 ) ) ) ) ) e. CC )
43 10 a1i 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> CC e. { RR , CC } )
44 c0ex 
 |-  0 e. _V
45 ovex 
 |-  ( k x. ( z ^ ( k - 1 ) ) ) e. _V
46 44 45 ifex 
 |-  if ( k = 0 , 0 , ( k x. ( z ^ ( k - 1 ) ) ) ) e. _V
47 46 a1i 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ z e. CC ) -> if ( k = 0 , 0 , ( k x. ( z ^ ( k - 1 ) ) ) ) e. _V )
48 17 adantl 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> k e. NN0 )
49 dvexp2 
 |-  ( k e. NN0 -> ( CC _D ( z e. CC |-> ( z ^ k ) ) ) = ( z e. CC |-> if ( k = 0 , 0 , ( k x. ( z ^ ( k - 1 ) ) ) ) ) )
50 48 49 syl 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( CC _D ( z e. CC |-> ( z ^ k ) ) ) = ( z e. CC |-> if ( k = 0 , 0 , ( k x. ( z ^ ( k - 1 ) ) ) ) ) )
51 43 23 47 50 19 dvmptcmul 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( CC _D ( z e. CC |-> ( ( A ` k ) x. ( z ^ k ) ) ) ) = ( z e. CC |-> ( ( A ` k ) x. if ( k = 0 , 0 , ( k x. ( z ^ ( k - 1 ) ) ) ) ) ) )
52 9 7 11 15 16 25 42 51 dvmptfsum 
 |-  ( ph -> ( CC _D ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. ( z ^ k ) ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. if ( k = 0 , 0 , ( k x. ( z ^ ( k - 1 ) ) ) ) ) ) )
53 elfznn 
 |-  ( k e. ( 1 ... N ) -> k e. NN )
54 53 nnne0d 
 |-  ( k e. ( 1 ... N ) -> k =/= 0 )
55 54 neneqd 
 |-  ( k e. ( 1 ... N ) -> -. k = 0 )
56 55 adantl 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 1 ... N ) ) -> -. k = 0 )
57 56 iffalsed 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 1 ... N ) ) -> if ( k = 0 , 0 , ( k x. ( z ^ ( k - 1 ) ) ) ) = ( k x. ( z ^ ( k - 1 ) ) ) )
58 57 oveq2d 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 1 ... N ) ) -> ( ( A ` k ) x. if ( k = 0 , 0 , ( k x. ( z ^ ( k - 1 ) ) ) ) ) = ( ( A ` k ) x. ( k x. ( z ^ ( k - 1 ) ) ) ) )
59 58 sumeq2dv 
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 1 ... N ) ( ( A ` k ) x. if ( k = 0 , 0 , ( k x. ( z ^ ( k - 1 ) ) ) ) ) = sum_ k e. ( 1 ... N ) ( ( A ` k ) x. ( k x. ( z ^ ( k - 1 ) ) ) ) )
60 1eluzge0 
 |-  1 e. ( ZZ>= ` 0 )
61 fzss1 
 |-  ( 1 e. ( ZZ>= ` 0 ) -> ( 1 ... N ) C_ ( 0 ... N ) )
62 60 61 mp1i 
 |-  ( ( ph /\ z e. CC ) -> ( 1 ... N ) C_ ( 0 ... N ) )
63 3 adantr 
 |-  ( ( ph /\ z e. CC ) -> A : NN0 --> CC )
64 53 nnnn0d 
 |-  ( k e. ( 1 ... N ) -> k e. NN0 )
65 63 64 18 syl2an 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 1 ... N ) ) -> ( A ` k ) e. CC )
66 54 adantl 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 1 ... N ) ) -> k =/= 0 )
67 66 neneqd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 1 ... N ) ) -> -. k = 0 )
68 67 iffalsed 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 1 ... N ) ) -> if ( k = 0 , 0 , ( k x. ( z ^ ( k - 1 ) ) ) ) = ( k x. ( z ^ ( k - 1 ) ) ) )
69 64 adantl 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 1 ... N ) ) -> k e. NN0 )
70 69 nn0cnd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 1 ... N ) ) -> k e. CC )
71 simplr 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 1 ... N ) ) -> z e. CC )
72 53 37 syl 
 |-  ( k e. ( 1 ... N ) -> ( k - 1 ) e. NN0 )
73 72 adantl 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 1 ... N ) ) -> ( k - 1 ) e. NN0 )
74 71 73 expcld 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 1 ... N ) ) -> ( z ^ ( k - 1 ) ) e. CC )
75 70 74 mulcld 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 1 ... N ) ) -> ( k x. ( z ^ ( k - 1 ) ) ) e. CC )
76 68 75 eqeltrd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 1 ... N ) ) -> if ( k = 0 , 0 , ( k x. ( z ^ ( k - 1 ) ) ) ) e. CC )
77 65 76 mulcld 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 1 ... N ) ) -> ( ( A ` k ) x. if ( k = 0 , 0 , ( k x. ( z ^ ( k - 1 ) ) ) ) ) e. CC )
78 eldifn 
 |-  ( k e. ( ( 0 ... N ) \ ( 1 ... N ) ) -> -. k e. ( 1 ... N ) )
79 0p1e1 
 |-  ( 0 + 1 ) = 1
80 79 oveq1i 
 |-  ( ( 0 + 1 ) ... N ) = ( 1 ... N )
81 80 eleq2i 
 |-  ( k e. ( ( 0 + 1 ) ... N ) <-> k e. ( 1 ... N ) )
82 78 81 sylnibr 
 |-  ( k e. ( ( 0 ... N ) \ ( 1 ... N ) ) -> -. k e. ( ( 0 + 1 ) ... N ) )
83 82 adantl 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... N ) \ ( 1 ... N ) ) ) -> -. k e. ( ( 0 + 1 ) ... N ) )
84 eldifi 
 |-  ( k e. ( ( 0 ... N ) \ ( 1 ... N ) ) -> k e. ( 0 ... N ) )
85 84 adantl 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... N ) \ ( 1 ... N ) ) ) -> k e. ( 0 ... N ) )
86 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
87 5 86 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 0 ) )
88 87 ad2antrr 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... N ) \ ( 1 ... N ) ) ) -> N e. ( ZZ>= ` 0 ) )
89 elfzp12 
 |-  ( N e. ( ZZ>= ` 0 ) -> ( k e. ( 0 ... N ) <-> ( k = 0 \/ k e. ( ( 0 + 1 ) ... N ) ) ) )
90 88 89 syl 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... N ) \ ( 1 ... N ) ) ) -> ( k e. ( 0 ... N ) <-> ( k = 0 \/ k e. ( ( 0 + 1 ) ... N ) ) ) )
91 85 90 mpbid 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... N ) \ ( 1 ... N ) ) ) -> ( k = 0 \/ k e. ( ( 0 + 1 ) ... N ) ) )
92 orel2 
 |-  ( -. k e. ( ( 0 + 1 ) ... N ) -> ( ( k = 0 \/ k e. ( ( 0 + 1 ) ... N ) ) -> k = 0 ) )
93 83 91 92 sylc 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... N ) \ ( 1 ... N ) ) ) -> k = 0 )
94 93 iftrued 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... N ) \ ( 1 ... N ) ) ) -> if ( k = 0 , 0 , ( k x. ( z ^ ( k - 1 ) ) ) ) = 0 )
95 94 oveq2d 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... N ) \ ( 1 ... N ) ) ) -> ( ( A ` k ) x. if ( k = 0 , 0 , ( k x. ( z ^ ( k - 1 ) ) ) ) ) = ( ( A ` k ) x. 0 ) )
96 63 17 18 syl2an 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... N ) ) -> ( A ` k ) e. CC )
97 96 mul01d 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... N ) ) -> ( ( A ` k ) x. 0 ) = 0 )
98 84 97 sylan2 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... N ) \ ( 1 ... N ) ) ) -> ( ( A ` k ) x. 0 ) = 0 )
99 95 98 eqtrd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... N ) \ ( 1 ... N ) ) ) -> ( ( A ` k ) x. if ( k = 0 , 0 , ( k x. ( z ^ ( k - 1 ) ) ) ) ) = 0 )
100 fzfid 
 |-  ( ( ph /\ z e. CC ) -> ( 0 ... N ) e. Fin )
101 62 77 99 100 fsumss 
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 1 ... N ) ( ( A ` k ) x. if ( k = 0 , 0 , ( k x. ( z ^ ( k - 1 ) ) ) ) ) = sum_ k e. ( 0 ... N ) ( ( A ` k ) x. if ( k = 0 , 0 , ( k x. ( z ^ ( k - 1 ) ) ) ) ) )
102 elfznn0 
 |-  ( j e. ( 0 ... ( N - 1 ) ) -> j e. NN0 )
103 102 adantl 
 |-  ( ( ( ph /\ z e. CC ) /\ j e. ( 0 ... ( N - 1 ) ) ) -> j e. NN0 )
104 103 nn0cnd 
 |-  ( ( ( ph /\ z e. CC ) /\ j e. ( 0 ... ( N - 1 ) ) ) -> j e. CC )
105 ax-1cn 
 |-  1 e. CC
106 pncan 
 |-  ( ( j e. CC /\ 1 e. CC ) -> ( ( j + 1 ) - 1 ) = j )
107 104 105 106 sylancl 
 |-  ( ( ( ph /\ z e. CC ) /\ j e. ( 0 ... ( N - 1 ) ) ) -> ( ( j + 1 ) - 1 ) = j )
108 107 oveq2d 
 |-  ( ( ( ph /\ z e. CC ) /\ j e. ( 0 ... ( N - 1 ) ) ) -> ( z ^ ( ( j + 1 ) - 1 ) ) = ( z ^ j ) )
109 108 oveq2d 
 |-  ( ( ( ph /\ z e. CC ) /\ j e. ( 0 ... ( N - 1 ) ) ) -> ( ( j + 1 ) x. ( z ^ ( ( j + 1 ) - 1 ) ) ) = ( ( j + 1 ) x. ( z ^ j ) ) )
110 109 oveq2d 
 |-  ( ( ( ph /\ z e. CC ) /\ j e. ( 0 ... ( N - 1 ) ) ) -> ( ( A ` ( j + 1 ) ) x. ( ( j + 1 ) x. ( z ^ ( ( j + 1 ) - 1 ) ) ) ) = ( ( A ` ( j + 1 ) ) x. ( ( j + 1 ) x. ( z ^ j ) ) ) )
111 3 ad2antrr 
 |-  ( ( ( ph /\ z e. CC ) /\ j e. ( 0 ... ( N - 1 ) ) ) -> A : NN0 --> CC )
112 peano2nn0 
 |-  ( j e. NN0 -> ( j + 1 ) e. NN0 )
113 102 112 syl 
 |-  ( j e. ( 0 ... ( N - 1 ) ) -> ( j + 1 ) e. NN0 )
114 113 adantl 
 |-  ( ( ( ph /\ z e. CC ) /\ j e. ( 0 ... ( N - 1 ) ) ) -> ( j + 1 ) e. NN0 )
115 111 114 ffvelcdmd 
 |-  ( ( ( ph /\ z e. CC ) /\ j e. ( 0 ... ( N - 1 ) ) ) -> ( A ` ( j + 1 ) ) e. CC )
116 114 nn0cnd 
 |-  ( ( ( ph /\ z e. CC ) /\ j e. ( 0 ... ( N - 1 ) ) ) -> ( j + 1 ) e. CC )
117 simplr 
 |-  ( ( ( ph /\ z e. CC ) /\ j e. ( 0 ... ( N - 1 ) ) ) -> z e. CC )
118 117 103 expcld 
 |-  ( ( ( ph /\ z e. CC ) /\ j e. ( 0 ... ( N - 1 ) ) ) -> ( z ^ j ) e. CC )
119 115 116 118 mulassd 
 |-  ( ( ( ph /\ z e. CC ) /\ j e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( A ` ( j + 1 ) ) x. ( j + 1 ) ) x. ( z ^ j ) ) = ( ( A ` ( j + 1 ) ) x. ( ( j + 1 ) x. ( z ^ j ) ) ) )
120 115 116 mulcomd 
 |-  ( ( ( ph /\ z e. CC ) /\ j e. ( 0 ... ( N - 1 ) ) ) -> ( ( A ` ( j + 1 ) ) x. ( j + 1 ) ) = ( ( j + 1 ) x. ( A ` ( j + 1 ) ) ) )
121 120 oveq1d 
 |-  ( ( ( ph /\ z e. CC ) /\ j e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( A ` ( j + 1 ) ) x. ( j + 1 ) ) x. ( z ^ j ) ) = ( ( ( j + 1 ) x. ( A ` ( j + 1 ) ) ) x. ( z ^ j ) ) )
122 110 119 121 3eqtr2d 
 |-  ( ( ( ph /\ z e. CC ) /\ j e. ( 0 ... ( N - 1 ) ) ) -> ( ( A ` ( j + 1 ) ) x. ( ( j + 1 ) x. ( z ^ ( ( j + 1 ) - 1 ) ) ) ) = ( ( ( j + 1 ) x. ( A ` ( j + 1 ) ) ) x. ( z ^ j ) ) )
123 122 sumeq2dv 
 |-  ( ( ph /\ z e. CC ) -> sum_ j e. ( 0 ... ( N - 1 ) ) ( ( A ` ( j + 1 ) ) x. ( ( j + 1 ) x. ( z ^ ( ( j + 1 ) - 1 ) ) ) ) = sum_ j e. ( 0 ... ( N - 1 ) ) ( ( ( j + 1 ) x. ( A ` ( j + 1 ) ) ) x. ( z ^ j ) ) )
124 1m1e0 
 |-  ( 1 - 1 ) = 0
125 124 oveq1i 
 |-  ( ( 1 - 1 ) ... ( N - 1 ) ) = ( 0 ... ( N - 1 ) )
126 125 sumeq1i 
 |-  sum_ j e. ( ( 1 - 1 ) ... ( N - 1 ) ) ( ( A ` ( j + 1 ) ) x. ( ( j + 1 ) x. ( z ^ ( ( j + 1 ) - 1 ) ) ) ) = sum_ j e. ( 0 ... ( N - 1 ) ) ( ( A ` ( j + 1 ) ) x. ( ( j + 1 ) x. ( z ^ ( ( j + 1 ) - 1 ) ) ) )
127 oveq1 
 |-  ( k = j -> ( k + 1 ) = ( j + 1 ) )
128 fvoveq1 
 |-  ( k = j -> ( A ` ( k + 1 ) ) = ( A ` ( j + 1 ) ) )
129 127 128 oveq12d 
 |-  ( k = j -> ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) = ( ( j + 1 ) x. ( A ` ( j + 1 ) ) ) )
130 oveq2 
 |-  ( k = j -> ( z ^ k ) = ( z ^ j ) )
131 129 130 oveq12d 
 |-  ( k = j -> ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( z ^ k ) ) = ( ( ( j + 1 ) x. ( A ` ( j + 1 ) ) ) x. ( z ^ j ) ) )
132 131 cbvsumv 
 |-  sum_ k e. ( 0 ... ( N - 1 ) ) ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( z ^ k ) ) = sum_ j e. ( 0 ... ( N - 1 ) ) ( ( ( j + 1 ) x. ( A ` ( j + 1 ) ) ) x. ( z ^ j ) )
133 123 126 132 3eqtr4g 
 |-  ( ( ph /\ z e. CC ) -> sum_ j e. ( ( 1 - 1 ) ... ( N - 1 ) ) ( ( A ` ( j + 1 ) ) x. ( ( j + 1 ) x. ( z ^ ( ( j + 1 ) - 1 ) ) ) ) = sum_ k e. ( 0 ... ( N - 1 ) ) ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( z ^ k ) ) )
134 1zzd 
 |-  ( ( ph /\ z e. CC ) -> 1 e. ZZ )
135 5 adantr 
 |-  ( ( ph /\ z e. CC ) -> N e. NN0 )
136 135 nn0zd 
 |-  ( ( ph /\ z e. CC ) -> N e. ZZ )
137 65 75 mulcld 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 1 ... N ) ) -> ( ( A ` k ) x. ( k x. ( z ^ ( k - 1 ) ) ) ) e. CC )
138 fveq2 
 |-  ( k = ( j + 1 ) -> ( A ` k ) = ( A ` ( j + 1 ) ) )
139 id 
 |-  ( k = ( j + 1 ) -> k = ( j + 1 ) )
140 oveq1 
 |-  ( k = ( j + 1 ) -> ( k - 1 ) = ( ( j + 1 ) - 1 ) )
141 140 oveq2d 
 |-  ( k = ( j + 1 ) -> ( z ^ ( k - 1 ) ) = ( z ^ ( ( j + 1 ) - 1 ) ) )
142 139 141 oveq12d 
 |-  ( k = ( j + 1 ) -> ( k x. ( z ^ ( k - 1 ) ) ) = ( ( j + 1 ) x. ( z ^ ( ( j + 1 ) - 1 ) ) ) )
143 138 142 oveq12d 
 |-  ( k = ( j + 1 ) -> ( ( A ` k ) x. ( k x. ( z ^ ( k - 1 ) ) ) ) = ( ( A ` ( j + 1 ) ) x. ( ( j + 1 ) x. ( z ^ ( ( j + 1 ) - 1 ) ) ) ) )
144 134 134 136 137 143 fsumshftm 
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 1 ... N ) ( ( A ` k ) x. ( k x. ( z ^ ( k - 1 ) ) ) ) = sum_ j e. ( ( 1 - 1 ) ... ( N - 1 ) ) ( ( A ` ( j + 1 ) ) x. ( ( j + 1 ) x. ( z ^ ( ( j + 1 ) - 1 ) ) ) ) )
145 elfznn0 
 |-  ( k e. ( 0 ... ( N - 1 ) ) -> k e. NN0 )
146 145 adantl 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> k e. NN0 )
147 ovex 
 |-  ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) e. _V
148 4 fvmpt2 
 |-  ( ( k e. NN0 /\ ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) e. _V ) -> ( B ` k ) = ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) )
149 146 147 148 sylancl 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( B ` k ) = ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) )
150 149 oveq1d 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( ( B ` k ) x. ( z ^ k ) ) = ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( z ^ k ) ) )
151 150 sumeq2dv 
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 0 ... ( N - 1 ) ) ( ( B ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... ( N - 1 ) ) ( ( ( k + 1 ) x. ( A ` ( k + 1 ) ) ) x. ( z ^ k ) ) )
152 133 144 151 3eqtr4d 
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 1 ... N ) ( ( A ` k ) x. ( k x. ( z ^ ( k - 1 ) ) ) ) = sum_ k e. ( 0 ... ( N - 1 ) ) ( ( B ` k ) x. ( z ^ k ) ) )
153 59 101 152 3eqtr3d 
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. if ( k = 0 , 0 , ( k x. ( z ^ ( k - 1 ) ) ) ) ) = sum_ k e. ( 0 ... ( N - 1 ) ) ( ( B ` k ) x. ( z ^ k ) ) )
154 153 mpteq2dva 
 |-  ( ph -> ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. if ( k = 0 , 0 , ( k x. ( z ^ ( k - 1 ) ) ) ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... ( N - 1 ) ) ( ( B ` k ) x. ( z ^ k ) ) ) )
155 154 2 eqtr4d 
 |-  ( ph -> ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( A ` k ) x. if ( k = 0 , 0 , ( k x. ( z ^ ( k - 1 ) ) ) ) ) ) = G )
156 6 52 155 3eqtrd 
 |-  ( ph -> ( CC _D F ) = G )