Metamath Proof Explorer

Theorem plymullem1

Description: Derive the coefficient function for the product of two polynomials. (Contributed by Mario Carneiro, 23-Jul-2014)

Ref Expression
Hypotheses plyaddlem.1 
|- ( ph -> F e. ( Poly ` S ) )
plyaddlem.2 
|- ( ph -> G e. ( Poly ` S ) )
plyaddlem.m 
|- ( ph -> M e. NN0 )
plyaddlem.n 
|- ( ph -> N e. NN0 )
plyaddlem.a 
|- ( ph -> A : NN0 --> CC )
plyaddlem.b 
|- ( ph -> B : NN0 --> CC )
plyaddlem.a2 
|- ( ph -> ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } )
plyaddlem.b2 
|- ( ph -> ( B " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
plyaddlem.f 
|- ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) ) )
plyaddlem.g 
|- ( ph -> G = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) ) )
Assertion plymullem1 
|- ( ph -> ( F oF x. G ) = ( z e. CC |-> sum_ n e. ( 0 ... ( M + N ) ) ( sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) x. ( z ^ n ) ) ) )

Proof

Step Hyp Ref Expression
1 plyaddlem.1 
 |-  ( ph -> F e. ( Poly ` S ) )
2 plyaddlem.2 
 |-  ( ph -> G e. ( Poly ` S ) )
3 plyaddlem.m 
 |-  ( ph -> M e. NN0 )
4 plyaddlem.n 
 |-  ( ph -> N e. NN0 )
5 plyaddlem.a 
 |-  ( ph -> A : NN0 --> CC )
6 plyaddlem.b 
 |-  ( ph -> B : NN0 --> CC )
7 plyaddlem.a2 
 |-  ( ph -> ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } )
8 plyaddlem.b2 
 |-  ( ph -> ( B " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
9 plyaddlem.f 
 |-  ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) ) )
10 plyaddlem.g 
 |-  ( ph -> G = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) ) )
11 cnex 
 |-  CC e. _V
12 11 a1i 
 |-  ( ph -> CC e. _V )
13 sumex 
 |-  sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) e. _V
14 13 a1i 
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) e. _V )
15 sumex 
 |-  sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) e. _V
16 15 a1i 
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) e. _V )
17 12 14 16 9 10 offval2 
 |-  ( ph -> ( F oF x. G ) = ( z e. CC |-> ( sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) x. sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) ) ) )
18 fveq2 
 |-  ( m = n -> ( B ` m ) = ( B ` n ) )
19 oveq2 
 |-  ( m = n -> ( z ^ m ) = ( z ^ n ) )
20 18 19 oveq12d 
 |-  ( m = n -> ( ( B ` m ) x. ( z ^ m ) ) = ( ( B ` n ) x. ( z ^ n ) ) )
21 20 oveq2d 
 |-  ( m = n -> ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` m ) x. ( z ^ m ) ) ) = ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) )
22 fveq2 
 |-  ( m = ( n - k ) -> ( B ` m ) = ( B ` ( n - k ) ) )
23 oveq2 
 |-  ( m = ( n - k ) -> ( z ^ m ) = ( z ^ ( n - k ) ) )
24 22 23 oveq12d 
 |-  ( m = ( n - k ) -> ( ( B ` m ) x. ( z ^ m ) ) = ( ( B ` ( n - k ) ) x. ( z ^ ( n - k ) ) ) )
25 24 oveq2d 
 |-  ( m = ( n - k ) -> ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` m ) x. ( z ^ m ) ) ) = ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` ( n - k ) ) x. ( z ^ ( n - k ) ) ) ) )
26 elfznn0 
 |-  ( k e. ( 0 ... ( M + N ) ) -> k e. NN0 )
27 5 adantr 
 |-  ( ( ph /\ z e. CC ) -> A : NN0 --> CC )
28 27 ffvelrnda 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. NN0 ) -> ( A ` k ) e. CC )
29 expcl 
 |-  ( ( z e. CC /\ k e. NN0 ) -> ( z ^ k ) e. CC )
30 29 adantll 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. NN0 ) -> ( z ^ k ) e. CC )
31 28 30 mulcld 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. NN0 ) -> ( ( A ` k ) x. ( z ^ k ) ) e. CC )
32 26 31 sylan2 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... ( M + N ) ) ) -> ( ( A ` k ) x. ( z ^ k ) ) e. CC )
33 elfznn0 
 |-  ( n e. ( 0 ... ( ( M + N ) - k ) ) -> n e. NN0 )
34 6 adantr 
 |-  ( ( ph /\ z e. CC ) -> B : NN0 --> CC )
35 34 ffvelrnda 
 |-  ( ( ( ph /\ z e. CC ) /\ n e. NN0 ) -> ( B ` n ) e. CC )
36 expcl 
 |-  ( ( z e. CC /\ n e. NN0 ) -> ( z ^ n ) e. CC )
37 36 adantll 
 |-  ( ( ( ph /\ z e. CC ) /\ n e. NN0 ) -> ( z ^ n ) e. CC )
38 35 37 mulcld 
 |-  ( ( ( ph /\ z e. CC ) /\ n e. NN0 ) -> ( ( B ` n ) x. ( z ^ n ) ) e. CC )
39 33 38 sylan2 
 |-  ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( ( M + N ) - k ) ) ) -> ( ( B ` n ) x. ( z ^ n ) ) e. CC )
40 32 39 anim12dan 
 |-  ( ( ( ph /\ z e. CC ) /\ ( k e. ( 0 ... ( M + N ) ) /\ n e. ( 0 ... ( ( M + N ) - k ) ) ) ) -> ( ( ( A ` k ) x. ( z ^ k ) ) e. CC /\ ( ( B ` n ) x. ( z ^ n ) ) e. CC ) )
41 mulcl 
 |-  ( ( ( ( A ` k ) x. ( z ^ k ) ) e. CC /\ ( ( B ` n ) x. ( z ^ n ) ) e. CC ) -> ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) e. CC )
42 40 41 syl 
 |-  ( ( ( ph /\ z e. CC ) /\ ( k e. ( 0 ... ( M + N ) ) /\ n e. ( 0 ... ( ( M + N ) - k ) ) ) ) -> ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) e. CC )
43 21 25 42 fsum0diag2 
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 0 ... ( M + N ) ) sum_ n e. ( 0 ... ( ( M + N ) - k ) ) ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) = sum_ n e. ( 0 ... ( M + N ) ) sum_ k e. ( 0 ... n ) ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` ( n - k ) ) x. ( z ^ ( n - k ) ) ) ) )
44 3 nn0cnd 
 |-  ( ph -> M e. CC )
45 44 ad2antrr 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> M e. CC )
46 4 nn0cnd 
 |-  ( ph -> N e. CC )
47 46 ad2antrr 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> N e. CC )
48 elfznn0 
 |-  ( k e. ( 0 ... M ) -> k e. NN0 )
49 48 adantl 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> k e. NN0 )
50 49 nn0cnd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> k e. CC )
51 45 47 50 addsubd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> ( ( M + N ) - k ) = ( ( M - k ) + N ) )
52 fznn0sub 
 |-  ( k e. ( 0 ... M ) -> ( M - k ) e. NN0 )
53 52 adantl 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> ( M - k ) e. NN0 )
54 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
55 53 54 eleqtrdi 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> ( M - k ) e. ( ZZ>= ` 0 ) )
56 4 nn0zd 
 |-  ( ph -> N e. ZZ )
57 56 ad2antrr 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> N e. ZZ )
58 eluzadd 
 |-  ( ( ( M - k ) e. ( ZZ>= ` 0 ) /\ N e. ZZ ) -> ( ( M - k ) + N ) e. ( ZZ>= ` ( 0 + N ) ) )
59 55 57 58 syl2anc 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> ( ( M - k ) + N ) e. ( ZZ>= ` ( 0 + N ) ) )
60 51 59 eqeltrd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> ( ( M + N ) - k ) e. ( ZZ>= ` ( 0 + N ) ) )
61 47 addid2d 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> ( 0 + N ) = N )
62 61 fveq2d 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> ( ZZ>= ` ( 0 + N ) ) = ( ZZ>= ` N ) )
63 60 62 eleqtrd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> ( ( M + N ) - k ) e. ( ZZ>= ` N ) )
64 fzss2 
 |-  ( ( ( M + N ) - k ) e. ( ZZ>= ` N ) -> ( 0 ... N ) C_ ( 0 ... ( ( M + N ) - k ) ) )
65 63 64 syl 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> ( 0 ... N ) C_ ( 0 ... ( ( M + N ) - k ) ) )
66 48 31 sylan2 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> ( ( A ` k ) x. ( z ^ k ) ) e. CC )
67 66 adantr 
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( 0 ... N ) ) -> ( ( A ` k ) x. ( z ^ k ) ) e. CC )
68 elfznn0 
 |-  ( n e. ( 0 ... N ) -> n e. NN0 )
69 68 38 sylan2 
 |-  ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... N ) ) -> ( ( B ` n ) x. ( z ^ n ) ) e. CC )
70 69 adantlr 
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( 0 ... N ) ) -> ( ( B ` n ) x. ( z ^ n ) ) e. CC )
71 67 70 mulcld 
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( 0 ... N ) ) -> ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) e. CC )
72 eldifn 
 |-  ( n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) -> -. n e. ( 0 ... N ) )
73 72 adantl 
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> -. n e. ( 0 ... N ) )
74 eldifi 
 |-  ( n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) -> n e. ( 0 ... ( ( M + N ) - k ) ) )
75 74 33 syl 
 |-  ( n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) -> n e. NN0 )
76 75 adantl 
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> n e. NN0 )
77 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
78 4 77 syl 
 |-  ( ph -> ( N + 1 ) e. NN0 )
79 78 54 eleqtrdi 
 |-  ( ph -> ( N + 1 ) e. ( ZZ>= ` 0 ) )
80 uzsplit 
 |-  ( ( N + 1 ) e. ( ZZ>= ` 0 ) -> ( ZZ>= ` 0 ) = ( ( 0 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) )
81 79 80 syl 
 |-  ( ph -> ( ZZ>= ` 0 ) = ( ( 0 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) )
82 54 81 syl5eq 
 |-  ( ph -> NN0 = ( ( 0 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) )
83 ax-1cn 
 |-  1 e. CC
84 pncan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N + 1 ) - 1 ) = N )
85 46 83 84 sylancl 
 |-  ( ph -> ( ( N + 1 ) - 1 ) = N )
86 85 oveq2d 
 |-  ( ph -> ( 0 ... ( ( N + 1 ) - 1 ) ) = ( 0 ... N ) )
87 86 uneq1d 
 |-  ( ph -> ( ( 0 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) = ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) )
88 82 87 eqtrd 
 |-  ( ph -> NN0 = ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) )
89 88 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> NN0 = ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) )
90 76 89 eleqtrd 
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> n e. ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) )
91 elun 
 |-  ( n e. ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) <-> ( n e. ( 0 ... N ) \/ n e. ( ZZ>= ` ( N + 1 ) ) ) )
92 90 91 sylib 
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> ( n e. ( 0 ... N ) \/ n e. ( ZZ>= ` ( N + 1 ) ) ) )
93 92 ord 
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> ( -. n e. ( 0 ... N ) -> n e. ( ZZ>= ` ( N + 1 ) ) ) )
94 73 93 mpd 
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> n e. ( ZZ>= ` ( N + 1 ) ) )
95 6 ffund 
 |-  ( ph -> Fun B )
96 ssun2 
 |-  ( ZZ>= ` ( N + 1 ) ) C_ ( ( 0 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) )
97 96 82 sseqtrrid 
 |-  ( ph -> ( ZZ>= ` ( N + 1 ) ) C_ NN0 )
98 6 fdmd 
 |-  ( ph -> dom B = NN0 )
99 97 98 sseqtrrd 
 |-  ( ph -> ( ZZ>= ` ( N + 1 ) ) C_ dom B )
100 funfvima2 
 |-  ( ( Fun B /\ ( ZZ>= ` ( N + 1 ) ) C_ dom B ) -> ( n e. ( ZZ>= ` ( N + 1 ) ) -> ( B ` n ) e. ( B " ( ZZ>= ` ( N + 1 ) ) ) ) )
101 95 99 100 syl2anc 
 |-  ( ph -> ( n e. ( ZZ>= ` ( N + 1 ) ) -> ( B ` n ) e. ( B " ( ZZ>= ` ( N + 1 ) ) ) ) )
102 101 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> ( n e. ( ZZ>= ` ( N + 1 ) ) -> ( B ` n ) e. ( B " ( ZZ>= ` ( N + 1 ) ) ) ) )
103 94 102 mpd 
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> ( B ` n ) e. ( B " ( ZZ>= ` ( N + 1 ) ) ) )
104 8 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> ( B " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
105 103 104 eleqtrd 
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> ( B ` n ) e. { 0 } )
106 elsni 
 |-  ( ( B ` n ) e. { 0 } -> ( B ` n ) = 0 )
107 105 106 syl 
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> ( B ` n ) = 0 )
108 107 oveq1d 
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> ( ( B ` n ) x. ( z ^ n ) ) = ( 0 x. ( z ^ n ) ) )
109 simplr 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> z e. CC )
110 109 75 36 syl2an 
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> ( z ^ n ) e. CC )
111 110 mul02d 
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> ( 0 x. ( z ^ n ) ) = 0 )
112 108 111 eqtrd 
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> ( ( B ` n ) x. ( z ^ n ) ) = 0 )
113 112 oveq2d 
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) = ( ( ( A ` k ) x. ( z ^ k ) ) x. 0 ) )
114 66 adantr 
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> ( ( A ` k ) x. ( z ^ k ) ) e. CC )
115 114 mul01d 
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> ( ( ( A ` k ) x. ( z ^ k ) ) x. 0 ) = 0 )
116 113 115 eqtrd 
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( ( 0 ... ( ( M + N ) - k ) ) \ ( 0 ... N ) ) ) -> ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) = 0 )
117 fzfid 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> ( 0 ... ( ( M + N ) - k ) ) e. Fin )
118 65 71 116 117 fsumss 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> sum_ n e. ( 0 ... N ) ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) = sum_ n e. ( 0 ... ( ( M + N ) - k ) ) ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) )
119 118 sumeq2dv 
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 0 ... M ) sum_ n e. ( 0 ... N ) ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) = sum_ k e. ( 0 ... M ) sum_ n e. ( 0 ... ( ( M + N ) - k ) ) ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) )
120 fzfid 
 |-  ( ( ph /\ z e. CC ) -> ( 0 ... M ) e. Fin )
121 fzfid 
 |-  ( ( ph /\ z e. CC ) -> ( 0 ... N ) e. Fin )
122 120 121 66 69 fsum2mul 
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 0 ... M ) sum_ n e. ( 0 ... N ) ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) = ( sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) x. sum_ n e. ( 0 ... N ) ( ( B ` n ) x. ( z ^ n ) ) ) )
123 44 46 addcomd 
 |-  ( ph -> ( M + N ) = ( N + M ) )
124 4 54 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 0 ) )
125 3 nn0zd 
 |-  ( ph -> M e. ZZ )
126 eluzadd 
 |-  ( ( N e. ( ZZ>= ` 0 ) /\ M e. ZZ ) -> ( N + M ) e. ( ZZ>= ` ( 0 + M ) ) )
127 124 125 126 syl2anc 
 |-  ( ph -> ( N + M ) e. ( ZZ>= ` ( 0 + M ) ) )
128 44 addid2d 
 |-  ( ph -> ( 0 + M ) = M )
129 128 fveq2d 
 |-  ( ph -> ( ZZ>= ` ( 0 + M ) ) = ( ZZ>= ` M ) )
130 127 129 eleqtrd 
 |-  ( ph -> ( N + M ) e. ( ZZ>= ` M ) )
131 123 130 eqeltrd 
 |-  ( ph -> ( M + N ) e. ( ZZ>= ` M ) )
132 fzss2 
 |-  ( ( M + N ) e. ( ZZ>= ` M ) -> ( 0 ... M ) C_ ( 0 ... ( M + N ) ) )
133 131 132 syl 
 |-  ( ph -> ( 0 ... M ) C_ ( 0 ... ( M + N ) ) )
134 133 adantr 
 |-  ( ( ph /\ z e. CC ) -> ( 0 ... M ) C_ ( 0 ... ( M + N ) ) )
135 66 adantr 
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( 0 ... ( ( M + N ) - k ) ) ) -> ( ( A ` k ) x. ( z ^ k ) ) e. CC )
136 39 adantlr 
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( 0 ... ( ( M + N ) - k ) ) ) -> ( ( B ` n ) x. ( z ^ n ) ) e. CC )
137 135 136 mulcld 
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) /\ n e. ( 0 ... ( ( M + N ) - k ) ) ) -> ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) e. CC )
138 117 137 fsumcl 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> sum_ n e. ( 0 ... ( ( M + N ) - k ) ) ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) e. CC )
139 eldifn 
 |-  ( k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) -> -. k e. ( 0 ... M ) )
140 139 adantl 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> -. k e. ( 0 ... M ) )
141 eldifi 
 |-  ( k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) -> k e. ( 0 ... ( M + N ) ) )
142 141 26 syl 
 |-  ( k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) -> k e. NN0 )
143 142 adantl 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> k e. NN0 )
144 peano2nn0 
 |-  ( M e. NN0 -> ( M + 1 ) e. NN0 )
145 3 144 syl 
 |-  ( ph -> ( M + 1 ) e. NN0 )
146 145 54 eleqtrdi 
 |-  ( ph -> ( M + 1 ) e. ( ZZ>= ` 0 ) )
147 uzsplit 
 |-  ( ( M + 1 ) e. ( ZZ>= ` 0 ) -> ( ZZ>= ` 0 ) = ( ( 0 ... ( ( M + 1 ) - 1 ) ) u. ( ZZ>= ` ( M + 1 ) ) ) )
148 146 147 syl 
 |-  ( ph -> ( ZZ>= ` 0 ) = ( ( 0 ... ( ( M + 1 ) - 1 ) ) u. ( ZZ>= ` ( M + 1 ) ) ) )
149 54 148 syl5eq 
 |-  ( ph -> NN0 = ( ( 0 ... ( ( M + 1 ) - 1 ) ) u. ( ZZ>= ` ( M + 1 ) ) ) )
150 pncan 
 |-  ( ( M e. CC /\ 1 e. CC ) -> ( ( M + 1 ) - 1 ) = M )
151 44 83 150 sylancl 
 |-  ( ph -> ( ( M + 1 ) - 1 ) = M )
152 151 oveq2d 
 |-  ( ph -> ( 0 ... ( ( M + 1 ) - 1 ) ) = ( 0 ... M ) )
153 152 uneq1d 
 |-  ( ph -> ( ( 0 ... ( ( M + 1 ) - 1 ) ) u. ( ZZ>= ` ( M + 1 ) ) ) = ( ( 0 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) )
154 149 153 eqtrd 
 |-  ( ph -> NN0 = ( ( 0 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) )
155 154 ad2antrr 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> NN0 = ( ( 0 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) )
156 143 155 eleqtrd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> k e. ( ( 0 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) )
157 elun 
 |-  ( k e. ( ( 0 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) <-> ( k e. ( 0 ... M ) \/ k e. ( ZZ>= ` ( M + 1 ) ) ) )
158 156 157 sylib 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> ( k e. ( 0 ... M ) \/ k e. ( ZZ>= ` ( M + 1 ) ) ) )
159 158 ord 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> ( -. k e. ( 0 ... M ) -> k e. ( ZZ>= ` ( M + 1 ) ) ) )
160 140 159 mpd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> k e. ( ZZ>= ` ( M + 1 ) ) )
161 5 ffund 
 |-  ( ph -> Fun A )
162 ssun2 
 |-  ( ZZ>= ` ( M + 1 ) ) C_ ( ( 0 ... ( ( M + 1 ) - 1 ) ) u. ( ZZ>= ` ( M + 1 ) ) )
163 162 149 sseqtrrid 
 |-  ( ph -> ( ZZ>= ` ( M + 1 ) ) C_ NN0 )
164 5 fdmd 
 |-  ( ph -> dom A = NN0 )
165 163 164 sseqtrrd 
 |-  ( ph -> ( ZZ>= ` ( M + 1 ) ) C_ dom A )
166 funfvima2 
 |-  ( ( Fun A /\ ( ZZ>= ` ( M + 1 ) ) C_ dom A ) -> ( k e. ( ZZ>= ` ( M + 1 ) ) -> ( A ` k ) e. ( A " ( ZZ>= ` ( M + 1 ) ) ) ) )
167 161 165 166 syl2anc 
 |-  ( ph -> ( k e. ( ZZ>= ` ( M + 1 ) ) -> ( A ` k ) e. ( A " ( ZZ>= ` ( M + 1 ) ) ) ) )
168 167 ad2antrr 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> ( k e. ( ZZ>= ` ( M + 1 ) ) -> ( A ` k ) e. ( A " ( ZZ>= ` ( M + 1 ) ) ) ) )
169 160 168 mpd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> ( A ` k ) e. ( A " ( ZZ>= ` ( M + 1 ) ) ) )
170 7 ad2antrr 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } )
171 169 170 eleqtrd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> ( A ` k ) e. { 0 } )
172 elsni 
 |-  ( ( A ` k ) e. { 0 } -> ( A ` k ) = 0 )
173 171 172 syl 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> ( A ` k ) = 0 )
174 173 oveq1d 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> ( ( A ` k ) x. ( z ^ k ) ) = ( 0 x. ( z ^ k ) ) )
175 142 30 sylan2 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> ( z ^ k ) e. CC )
176 175 mul02d 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> ( 0 x. ( z ^ k ) ) = 0 )
177 174 176 eqtrd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> ( ( A ` k ) x. ( z ^ k ) ) = 0 )
178 177 adantr 
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) /\ n e. ( 0 ... ( ( M + N ) - k ) ) ) -> ( ( A ` k ) x. ( z ^ k ) ) = 0 )
179 178 oveq1d 
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) /\ n e. ( 0 ... ( ( M + N ) - k ) ) ) -> ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) = ( 0 x. ( ( B ` n ) x. ( z ^ n ) ) ) )
180 39 adantlr 
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) /\ n e. ( 0 ... ( ( M + N ) - k ) ) ) -> ( ( B ` n ) x. ( z ^ n ) ) e. CC )
181 180 mul02d 
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) /\ n e. ( 0 ... ( ( M + N ) - k ) ) ) -> ( 0 x. ( ( B ` n ) x. ( z ^ n ) ) ) = 0 )
182 179 181 eqtrd 
 |-  ( ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) /\ n e. ( 0 ... ( ( M + N ) - k ) ) ) -> ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) = 0 )
183 182 sumeq2dv 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> sum_ n e. ( 0 ... ( ( M + N ) - k ) ) ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) = sum_ n e. ( 0 ... ( ( M + N ) - k ) ) 0 )
184 fzfid 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> ( 0 ... ( ( M + N ) - k ) ) e. Fin )
185 184 olcd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> ( ( 0 ... ( ( M + N ) - k ) ) C_ ( ZZ>= ` 0 ) \/ ( 0 ... ( ( M + N ) - k ) ) e. Fin ) )
186 sumz 
 |-  ( ( ( 0 ... ( ( M + N ) - k ) ) C_ ( ZZ>= ` 0 ) \/ ( 0 ... ( ( M + N ) - k ) ) e. Fin ) -> sum_ n e. ( 0 ... ( ( M + N ) - k ) ) 0 = 0 )
187 185 186 syl 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> sum_ n e. ( 0 ... ( ( M + N ) - k ) ) 0 = 0 )
188 183 187 eqtrd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> sum_ n e. ( 0 ... ( ( M + N ) - k ) ) ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) = 0 )
189 fzfid 
 |-  ( ( ph /\ z e. CC ) -> ( 0 ... ( M + N ) ) e. Fin )
190 134 138 188 189 fsumss 
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 0 ... M ) sum_ n e. ( 0 ... ( ( M + N ) - k ) ) ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) = sum_ k e. ( 0 ... ( M + N ) ) sum_ n e. ( 0 ... ( ( M + N ) - k ) ) ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) )
191 119 122 190 3eqtr3d 
 |-  ( ( ph /\ z e. CC ) -> ( sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) x. sum_ n e. ( 0 ... N ) ( ( B ` n ) x. ( z ^ n ) ) ) = sum_ k e. ( 0 ... ( M + N ) ) sum_ n e. ( 0 ... ( ( M + N ) - k ) ) ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` n ) x. ( z ^ n ) ) ) )
192 fzfid 
 |-  ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) -> ( 0 ... n ) e. Fin )
193 elfznn0 
 |-  ( n e. ( 0 ... ( M + N ) ) -> n e. NN0 )
194 193 37 sylan2 
 |-  ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) -> ( z ^ n ) e. CC )
195 simpll 
 |-  ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) -> ph )
196 elfznn0 
 |-  ( k e. ( 0 ... n ) -> k e. NN0 )
197 5 ffvelrnda 
 |-  ( ( ph /\ k e. NN0 ) -> ( A ` k ) e. CC )
198 195 196 197 syl2an 
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> ( A ` k ) e. CC )
199 fznn0sub 
 |-  ( k e. ( 0 ... n ) -> ( n - k ) e. NN0 )
200 6 ffvelrnda 
 |-  ( ( ph /\ ( n - k ) e. NN0 ) -> ( B ` ( n - k ) ) e. CC )
201 195 199 200 syl2an 
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> ( B ` ( n - k ) ) e. CC )
202 198 201 mulcld 
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> ( ( A ` k ) x. ( B ` ( n - k ) ) ) e. CC )
203 192 194 202 fsummulc1 
 |-  ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) -> ( sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) x. ( z ^ n ) ) = sum_ k e. ( 0 ... n ) ( ( ( A ` k ) x. ( B ` ( n - k ) ) ) x. ( z ^ n ) ) )
204 simplr 
 |-  ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) -> z e. CC )
205 204 196 29 syl2an 
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> ( z ^ k ) e. CC )
206 expcl 
 |-  ( ( z e. CC /\ ( n - k ) e. NN0 ) -> ( z ^ ( n - k ) ) e. CC )
207 204 199 206 syl2an 
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> ( z ^ ( n - k ) ) e. CC )
208 198 205 201 207 mul4d 
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` ( n - k ) ) x. ( z ^ ( n - k ) ) ) ) = ( ( ( A ` k ) x. ( B ` ( n - k ) ) ) x. ( ( z ^ k ) x. ( z ^ ( n - k ) ) ) ) )
209 204 adantr 
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> z e. CC )
210 199 adantl 
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> ( n - k ) e. NN0 )
211 196 adantl 
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> k e. NN0 )
212 209 210 211 expaddd 
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> ( z ^ ( k + ( n - k ) ) ) = ( ( z ^ k ) x. ( z ^ ( n - k ) ) ) )
213 211 nn0cnd 
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> k e. CC )
214 193 ad2antlr 
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> n e. NN0 )
215 214 nn0cnd 
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> n e. CC )
216 213 215 pncan3d 
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> ( k + ( n - k ) ) = n )
217 216 oveq2d 
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> ( z ^ ( k + ( n - k ) ) ) = ( z ^ n ) )
218 212 217 eqtr3d 
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> ( ( z ^ k ) x. ( z ^ ( n - k ) ) ) = ( z ^ n ) )
219 218 oveq2d 
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> ( ( ( A ` k ) x. ( B ` ( n - k ) ) ) x. ( ( z ^ k ) x. ( z ^ ( n - k ) ) ) ) = ( ( ( A ` k ) x. ( B ` ( n - k ) ) ) x. ( z ^ n ) ) )
220 208 219 eqtrd 
 |-  ( ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) /\ k e. ( 0 ... n ) ) -> ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` ( n - k ) ) x. ( z ^ ( n - k ) ) ) ) = ( ( ( A ` k ) x. ( B ` ( n - k ) ) ) x. ( z ^ n ) ) )
221 220 sumeq2dv 
 |-  ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) -> sum_ k e. ( 0 ... n ) ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` ( n - k ) ) x. ( z ^ ( n - k ) ) ) ) = sum_ k e. ( 0 ... n ) ( ( ( A ` k ) x. ( B ` ( n - k ) ) ) x. ( z ^ n ) ) )
222 203 221 eqtr4d 
 |-  ( ( ( ph /\ z e. CC ) /\ n e. ( 0 ... ( M + N ) ) ) -> ( sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) x. ( z ^ n ) ) = sum_ k e. ( 0 ... n ) ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` ( n - k ) ) x. ( z ^ ( n - k ) ) ) ) )
223 222 sumeq2dv 
 |-  ( ( ph /\ z e. CC ) -> sum_ n e. ( 0 ... ( M + N ) ) ( sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) x. ( z ^ n ) ) = sum_ n e. ( 0 ... ( M + N ) ) sum_ k e. ( 0 ... n ) ( ( ( A ` k ) x. ( z ^ k ) ) x. ( ( B ` ( n - k ) ) x. ( z ^ ( n - k ) ) ) ) )
224 43 191 223 3eqtr4rd 
 |-  ( ( ph /\ z e. CC ) -> sum_ n e. ( 0 ... ( M + N ) ) ( sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) x. ( z ^ n ) ) = ( sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) x. sum_ n e. ( 0 ... N ) ( ( B ` n ) x. ( z ^ n ) ) ) )
225 fveq2 
 |-  ( n = k -> ( B ` n ) = ( B ` k ) )
226 oveq2 
 |-  ( n = k -> ( z ^ n ) = ( z ^ k ) )
227 225 226 oveq12d 
 |-  ( n = k -> ( ( B ` n ) x. ( z ^ n ) ) = ( ( B ` k ) x. ( z ^ k ) ) )
228 227 cbvsumv 
 |-  sum_ n e. ( 0 ... N ) ( ( B ` n ) x. ( z ^ n ) ) = sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) )
229 228 oveq2i 
 |-  ( sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) x. sum_ n e. ( 0 ... N ) ( ( B ` n ) x. ( z ^ n ) ) ) = ( sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) x. sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) )
230 224 229 eqtrdi 
 |-  ( ( ph /\ z e. CC ) -> sum_ n e. ( 0 ... ( M + N ) ) ( sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) x. ( z ^ n ) ) = ( sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) x. sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) ) )
231 230 mpteq2dva 
 |-  ( ph -> ( z e. CC |-> sum_ n e. ( 0 ... ( M + N ) ) ( sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) x. ( z ^ n ) ) ) = ( z e. CC |-> ( sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) x. sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) ) ) )
232 17 231 eqtr4d 
 |-  ( ph -> ( F oF x. G ) = ( z e. CC |-> sum_ n e. ( 0 ... ( M + N ) ) ( sum_ k e. ( 0 ... n ) ( ( A ` k ) x. ( B ` ( n - k ) ) ) x. ( z ^ n ) ) ) )