Metamath Proof Explorer

Theorem plyaddlem1

Description: Derive the coefficient function for the sum 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 plyaddlem1 
|- ( ph -> ( F oF + G ) = ( z e. CC |-> sum_ k e. ( 0 ... if ( M <_ N , N , M ) ) ( ( ( A oF + B ) ` k ) x. ( z ^ k ) ) ) )

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 + G ) = ( z e. CC |-> ( sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) + sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) ) ) )
18 fzfid 
 |-  ( ( ph /\ z e. CC ) -> ( 0 ... if ( M <_ N , N , M ) ) e. Fin )
19 elfznn0 
 |-  ( k e. ( 0 ... if ( M <_ N , N , M ) ) -> k e. NN0 )
20 5 adantr 
 |-  ( ( ph /\ z e. CC ) -> A : NN0 --> CC )
21 20 ffvelcdmda 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. NN0 ) -> ( A ` k ) e. CC )
22 expcl 
 |-  ( ( z e. CC /\ k e. NN0 ) -> ( z ^ k ) e. CC )
23 22 adantll 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. NN0 ) -> ( z ^ k ) e. CC )
24 21 23 mulcld 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. NN0 ) -> ( ( A ` k ) x. ( z ^ k ) ) e. CC )
25 19 24 sylan2 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... if ( M <_ N , N , M ) ) ) -> ( ( A ` k ) x. ( z ^ k ) ) e. CC )
26 6 adantr 
 |-  ( ( ph /\ z e. CC ) -> B : NN0 --> CC )
27 26 ffvelcdmda 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. NN0 ) -> ( B ` k ) e. CC )
28 27 23 mulcld 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. NN0 ) -> ( ( B ` k ) x. ( z ^ k ) ) e. CC )
29 19 28 sylan2 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... if ( M <_ N , N , M ) ) ) -> ( ( B ` k ) x. ( z ^ k ) ) e. CC )
30 18 25 29 fsumadd 
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 0 ... if ( M <_ N , N , M ) ) ( ( ( A ` k ) x. ( z ^ k ) ) + ( ( B ` k ) x. ( z ^ k ) ) ) = ( sum_ k e. ( 0 ... if ( M <_ N , N , M ) ) ( ( A ` k ) x. ( z ^ k ) ) + sum_ k e. ( 0 ... if ( M <_ N , N , M ) ) ( ( B ` k ) x. ( z ^ k ) ) ) )
31 5 ffnd 
 |-  ( ph -> A Fn NN0 )
32 6 ffnd 
 |-  ( ph -> B Fn NN0 )
33 nn0ex 
 |-  NN0 e. _V
34 33 a1i 
 |-  ( ph -> NN0 e. _V )
35 inidm 
 |-  ( NN0 i^i NN0 ) = NN0
36 eqidd 
 |-  ( ( ph /\ k e. NN0 ) -> ( A ` k ) = ( A ` k ) )
37 eqidd 
 |-  ( ( ph /\ k e. NN0 ) -> ( B ` k ) = ( B ` k ) )
38 31 32 34 34 35 36 37 ofval 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( A oF + B ) ` k ) = ( ( A ` k ) + ( B ` k ) ) )
39 38 adantlr 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. NN0 ) -> ( ( A oF + B ) ` k ) = ( ( A ` k ) + ( B ` k ) ) )
40 39 oveq1d 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. NN0 ) -> ( ( ( A oF + B ) ` k ) x. ( z ^ k ) ) = ( ( ( A ` k ) + ( B ` k ) ) x. ( z ^ k ) ) )
41 21 27 23 adddird 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. NN0 ) -> ( ( ( A ` k ) + ( B ` k ) ) x. ( z ^ k ) ) = ( ( ( A ` k ) x. ( z ^ k ) ) + ( ( B ` k ) x. ( z ^ k ) ) ) )
42 40 41 eqtrd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. NN0 ) -> ( ( ( A oF + B ) ` k ) x. ( z ^ k ) ) = ( ( ( A ` k ) x. ( z ^ k ) ) + ( ( B ` k ) x. ( z ^ k ) ) ) )
43 19 42 sylan2 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... if ( M <_ N , N , M ) ) ) -> ( ( ( A oF + B ) ` k ) x. ( z ^ k ) ) = ( ( ( A ` k ) x. ( z ^ k ) ) + ( ( B ` k ) x. ( z ^ k ) ) ) )
44 43 sumeq2dv 
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 0 ... if ( M <_ N , N , M ) ) ( ( ( A oF + B ) ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... if ( M <_ N , N , M ) ) ( ( ( A ` k ) x. ( z ^ k ) ) + ( ( B ` k ) x. ( z ^ k ) ) ) )
45 3 nn0zd 
 |-  ( ph -> M e. ZZ )
46 4 3 ifcld 
 |-  ( ph -> if ( M <_ N , N , M ) e. NN0 )
47 46 nn0zd 
 |-  ( ph -> if ( M <_ N , N , M ) e. ZZ )
48 3 nn0red 
 |-  ( ph -> M e. RR )
49 4 nn0red 
 |-  ( ph -> N e. RR )
50 max1 
 |-  ( ( M e. RR /\ N e. RR ) -> M <_ if ( M <_ N , N , M ) )
51 48 49 50 syl2anc 
 |-  ( ph -> M <_ if ( M <_ N , N , M ) )
52 eluz2 
 |-  ( if ( M <_ N , N , M ) e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ if ( M <_ N , N , M ) e. ZZ /\ M <_ if ( M <_ N , N , M ) ) )
53 45 47 51 52 syl3anbrc 
 |-  ( ph -> if ( M <_ N , N , M ) e. ( ZZ>= ` M ) )
54 fzss2 
 |-  ( if ( M <_ N , N , M ) e. ( ZZ>= ` M ) -> ( 0 ... M ) C_ ( 0 ... if ( M <_ N , N , M ) ) )
55 53 54 syl 
 |-  ( ph -> ( 0 ... M ) C_ ( 0 ... if ( M <_ N , N , M ) ) )
56 55 adantr 
 |-  ( ( ph /\ z e. CC ) -> ( 0 ... M ) C_ ( 0 ... if ( M <_ N , N , M ) ) )
57 elfznn0 
 |-  ( k e. ( 0 ... M ) -> k e. NN0 )
58 57 24 sylan2 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> ( ( A ` k ) x. ( z ^ k ) ) e. CC )
59 eldifn 
 |-  ( k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... M ) ) -> -. k e. ( 0 ... M ) )
60 59 adantl 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... M ) ) ) -> -. k e. ( 0 ... M ) )
61 eldifi 
 |-  ( k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... M ) ) -> k e. ( 0 ... if ( M <_ N , N , M ) ) )
62 61 19 syl 
 |-  ( k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... M ) ) -> k e. NN0 )
63 62 adantl 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... M ) ) ) -> k e. NN0 )
64 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
65 peano2nn0 
 |-  ( M e. NN0 -> ( M + 1 ) e. NN0 )
66 3 65 syl 
 |-  ( ph -> ( M + 1 ) e. NN0 )
67 66 64 eleqtrdi 
 |-  ( ph -> ( M + 1 ) e. ( ZZ>= ` 0 ) )
68 uzsplit 
 |-  ( ( M + 1 ) e. ( ZZ>= ` 0 ) -> ( ZZ>= ` 0 ) = ( ( 0 ... ( ( M + 1 ) - 1 ) ) u. ( ZZ>= ` ( M + 1 ) ) ) )
69 67 68 syl 
 |-  ( ph -> ( ZZ>= ` 0 ) = ( ( 0 ... ( ( M + 1 ) - 1 ) ) u. ( ZZ>= ` ( M + 1 ) ) ) )
70 64 69 eqtrid 
 |-  ( ph -> NN0 = ( ( 0 ... ( ( M + 1 ) - 1 ) ) u. ( ZZ>= ` ( M + 1 ) ) ) )
71 3 nn0cnd 
 |-  ( ph -> M e. CC )
72 ax-1cn 
 |-  1 e. CC
73 pncan 
 |-  ( ( M e. CC /\ 1 e. CC ) -> ( ( M + 1 ) - 1 ) = M )
74 71 72 73 sylancl 
 |-  ( ph -> ( ( M + 1 ) - 1 ) = M )
75 74 oveq2d 
 |-  ( ph -> ( 0 ... ( ( M + 1 ) - 1 ) ) = ( 0 ... M ) )
76 75 uneq1d 
 |-  ( ph -> ( ( 0 ... ( ( M + 1 ) - 1 ) ) u. ( ZZ>= ` ( M + 1 ) ) ) = ( ( 0 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) )
77 70 76 eqtrd 
 |-  ( ph -> NN0 = ( ( 0 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) )
78 77 ad2antrr 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... M ) ) ) -> NN0 = ( ( 0 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) )
79 63 78 eleqtrd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... M ) ) ) -> k e. ( ( 0 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) )
80 elun 
 |-  ( k e. ( ( 0 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) <-> ( k e. ( 0 ... M ) \/ k e. ( ZZ>= ` ( M + 1 ) ) ) )
81 79 80 sylib 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... M ) ) ) -> ( k e. ( 0 ... M ) \/ k e. ( ZZ>= ` ( M + 1 ) ) ) )
82 81 ord 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... M ) ) ) -> ( -. k e. ( 0 ... M ) -> k e. ( ZZ>= ` ( M + 1 ) ) ) )
83 60 82 mpd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... M ) ) ) -> k e. ( ZZ>= ` ( M + 1 ) ) )
84 5 ffund 
 |-  ( ph -> Fun A )
85 ssun2 
 |-  ( ZZ>= ` ( M + 1 ) ) C_ ( ( 0 ... ( ( M + 1 ) - 1 ) ) u. ( ZZ>= ` ( M + 1 ) ) )
86 85 70 sseqtrrid 
 |-  ( ph -> ( ZZ>= ` ( M + 1 ) ) C_ NN0 )
87 5 fdmd 
 |-  ( ph -> dom A = NN0 )
88 86 87 sseqtrrd 
 |-  ( ph -> ( ZZ>= ` ( M + 1 ) ) C_ dom A )
89 funfvima2 
 |-  ( ( Fun A /\ ( ZZ>= ` ( M + 1 ) ) C_ dom A ) -> ( k e. ( ZZ>= ` ( M + 1 ) ) -> ( A ` k ) e. ( A " ( ZZ>= ` ( M + 1 ) ) ) ) )
90 84 88 89 syl2anc 
 |-  ( ph -> ( k e. ( ZZ>= ` ( M + 1 ) ) -> ( A ` k ) e. ( A " ( ZZ>= ` ( M + 1 ) ) ) ) )
91 90 ad2antrr 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... M ) ) ) -> ( k e. ( ZZ>= ` ( M + 1 ) ) -> ( A ` k ) e. ( A " ( ZZ>= ` ( M + 1 ) ) ) ) )
92 83 91 mpd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... M ) ) ) -> ( A ` k ) e. ( A " ( ZZ>= ` ( M + 1 ) ) ) )
93 7 ad2antrr 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... M ) ) ) -> ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } )
94 92 93 eleqtrd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... M ) ) ) -> ( A ` k ) e. { 0 } )
95 elsni 
 |-  ( ( A ` k ) e. { 0 } -> ( A ` k ) = 0 )
96 94 95 syl 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... M ) ) ) -> ( A ` k ) = 0 )
97 96 oveq1d 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... M ) ) ) -> ( ( A ` k ) x. ( z ^ k ) ) = ( 0 x. ( z ^ k ) ) )
98 62 23 sylan2 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... M ) ) ) -> ( z ^ k ) e. CC )
99 98 mul02d 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... M ) ) ) -> ( 0 x. ( z ^ k ) ) = 0 )
100 97 99 eqtrd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... M ) ) ) -> ( ( A ` k ) x. ( z ^ k ) ) = 0 )
101 56 58 100 18 fsumss 
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... if ( M <_ N , N , M ) ) ( ( A ` k ) x. ( z ^ k ) ) )
102 4 nn0zd 
 |-  ( ph -> N e. ZZ )
103 max2 
 |-  ( ( M e. RR /\ N e. RR ) -> N <_ if ( M <_ N , N , M ) )
104 48 49 103 syl2anc 
 |-  ( ph -> N <_ if ( M <_ N , N , M ) )
105 eluz2 
 |-  ( if ( M <_ N , N , M ) e. ( ZZ>= ` N ) <-> ( N e. ZZ /\ if ( M <_ N , N , M ) e. ZZ /\ N <_ if ( M <_ N , N , M ) ) )
106 102 47 104 105 syl3anbrc 
 |-  ( ph -> if ( M <_ N , N , M ) e. ( ZZ>= ` N ) )
107 fzss2 
 |-  ( if ( M <_ N , N , M ) e. ( ZZ>= ` N ) -> ( 0 ... N ) C_ ( 0 ... if ( M <_ N , N , M ) ) )
108 106 107 syl 
 |-  ( ph -> ( 0 ... N ) C_ ( 0 ... if ( M <_ N , N , M ) ) )
109 108 adantr 
 |-  ( ( ph /\ z e. CC ) -> ( 0 ... N ) C_ ( 0 ... if ( M <_ N , N , M ) ) )
110 elfznn0 
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
111 110 28 sylan2 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... N ) ) -> ( ( B ` k ) x. ( z ^ k ) ) e. CC )
112 eldifn 
 |-  ( k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... N ) ) -> -. k e. ( 0 ... N ) )
113 112 adantl 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... N ) ) ) -> -. k e. ( 0 ... N ) )
114 eldifi 
 |-  ( k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... N ) ) -> k e. ( 0 ... if ( M <_ N , N , M ) ) )
115 114 19 syl 
 |-  ( k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... N ) ) -> k e. NN0 )
116 115 adantl 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... N ) ) ) -> k e. NN0 )
117 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
118 4 117 syl 
 |-  ( ph -> ( N + 1 ) e. NN0 )
119 118 64 eleqtrdi 
 |-  ( ph -> ( N + 1 ) e. ( ZZ>= ` 0 ) )
120 uzsplit 
 |-  ( ( N + 1 ) e. ( ZZ>= ` 0 ) -> ( ZZ>= ` 0 ) = ( ( 0 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) )
121 119 120 syl 
 |-  ( ph -> ( ZZ>= ` 0 ) = ( ( 0 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) )
122 64 121 eqtrid 
 |-  ( ph -> NN0 = ( ( 0 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) )
123 4 nn0cnd 
 |-  ( ph -> N e. CC )
124 pncan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N + 1 ) - 1 ) = N )
125 123 72 124 sylancl 
 |-  ( ph -> ( ( N + 1 ) - 1 ) = N )
126 125 oveq2d 
 |-  ( ph -> ( 0 ... ( ( N + 1 ) - 1 ) ) = ( 0 ... N ) )
127 126 uneq1d 
 |-  ( ph -> ( ( 0 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) ) = ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) )
128 122 127 eqtrd 
 |-  ( ph -> NN0 = ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) )
129 128 ad2antrr 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... N ) ) ) -> NN0 = ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) )
130 116 129 eleqtrd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... N ) ) ) -> k e. ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) )
131 elun 
 |-  ( k e. ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) <-> ( k e. ( 0 ... N ) \/ k e. ( ZZ>= ` ( N + 1 ) ) ) )
132 130 131 sylib 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... N ) ) ) -> ( k e. ( 0 ... N ) \/ k e. ( ZZ>= ` ( N + 1 ) ) ) )
133 132 ord 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... N ) ) ) -> ( -. k e. ( 0 ... N ) -> k e. ( ZZ>= ` ( N + 1 ) ) ) )
134 113 133 mpd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... N ) ) ) -> k e. ( ZZ>= ` ( N + 1 ) ) )
135 6 ffund 
 |-  ( ph -> Fun B )
136 ssun2 
 |-  ( ZZ>= ` ( N + 1 ) ) C_ ( ( 0 ... ( ( N + 1 ) - 1 ) ) u. ( ZZ>= ` ( N + 1 ) ) )
137 136 122 sseqtrrid 
 |-  ( ph -> ( ZZ>= ` ( N + 1 ) ) C_ NN0 )
138 6 fdmd 
 |-  ( ph -> dom B = NN0 )
139 137 138 sseqtrrd 
 |-  ( ph -> ( ZZ>= ` ( N + 1 ) ) C_ dom B )
140 funfvima2 
 |-  ( ( Fun B /\ ( ZZ>= ` ( N + 1 ) ) C_ dom B ) -> ( k e. ( ZZ>= ` ( N + 1 ) ) -> ( B ` k ) e. ( B " ( ZZ>= ` ( N + 1 ) ) ) ) )
141 135 139 140 syl2anc 
 |-  ( ph -> ( k e. ( ZZ>= ` ( N + 1 ) ) -> ( B ` k ) e. ( B " ( ZZ>= ` ( N + 1 ) ) ) ) )
142 141 ad2antrr 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... N ) ) ) -> ( k e. ( ZZ>= ` ( N + 1 ) ) -> ( B ` k ) e. ( B " ( ZZ>= ` ( N + 1 ) ) ) ) )
143 134 142 mpd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... N ) ) ) -> ( B ` k ) e. ( B " ( ZZ>= ` ( N + 1 ) ) ) )
144 8 ad2antrr 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... N ) ) ) -> ( B " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
145 143 144 eleqtrd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... N ) ) ) -> ( B ` k ) e. { 0 } )
146 elsni 
 |-  ( ( B ` k ) e. { 0 } -> ( B ` k ) = 0 )
147 145 146 syl 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... N ) ) ) -> ( B ` k ) = 0 )
148 147 oveq1d 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... N ) ) ) -> ( ( B ` k ) x. ( z ^ k ) ) = ( 0 x. ( z ^ k ) ) )
149 115 23 sylan2 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... N ) ) ) -> ( z ^ k ) e. CC )
150 149 mul02d 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... N ) ) ) -> ( 0 x. ( z ^ k ) ) = 0 )
151 148 150 eqtrd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... if ( M <_ N , N , M ) ) \ ( 0 ... N ) ) ) -> ( ( B ` k ) x. ( z ^ k ) ) = 0 )
152 109 111 151 18 fsumss 
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... if ( M <_ N , N , M ) ) ( ( B ` k ) x. ( z ^ k ) ) )
153 101 152 oveq12d 
 |-  ( ( ph /\ z e. CC ) -> ( sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) + sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) ) = ( sum_ k e. ( 0 ... if ( M <_ N , N , M ) ) ( ( A ` k ) x. ( z ^ k ) ) + sum_ k e. ( 0 ... if ( M <_ N , N , M ) ) ( ( B ` k ) x. ( z ^ k ) ) ) )
154 30 44 153 3eqtr4d 
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 0 ... if ( M <_ N , N , M ) ) ( ( ( A oF + B ) ` k ) x. ( z ^ k ) ) = ( sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) + sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) ) )
155 154 mpteq2dva 
 |-  ( ph -> ( z e. CC |-> sum_ k e. ( 0 ... if ( M <_ N , N , M ) ) ( ( ( A oF + B ) ` k ) x. ( z ^ k ) ) ) = ( z e. CC |-> ( sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) + sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) ) ) )
156 17 155 eqtr4d 
 |-  ( ph -> ( F oF + G ) = ( z e. CC |-> sum_ k e. ( 0 ... if ( M <_ N , N , M ) ) ( ( ( A oF + B ) ` k ) x. ( z ^ k ) ) ) )