Metamath Proof Explorer

Theorem coeeulem

Description: Lemma for coeeu . (Contributed by Mario Carneiro, 22-Jul-2014)

Ref Expression
Hypotheses coeeu.1 
|- ( ph -> F e. ( Poly ` S ) )
coeeu.2 
|- ( ph -> A e. ( CC ^m NN0 ) )
coeeu.3 
|- ( ph -> B e. ( CC ^m NN0 ) )
coeeu.4 
|- ( ph -> M e. NN0 )
coeeu.5 
|- ( ph -> N e. NN0 )
coeeu.6 
|- ( ph -> ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } )
coeeu.7 
|- ( ph -> ( B " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
coeeu.8 
|- ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) ) )
coeeu.9 
|- ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) ) )
Assertion coeeulem 
|- ( ph -> A = B )

Proof

Step Hyp Ref Expression
1 coeeu.1 
 |-  ( ph -> F e. ( Poly ` S ) )
2 coeeu.2 
 |-  ( ph -> A e. ( CC ^m NN0 ) )
3 coeeu.3 
 |-  ( ph -> B e. ( CC ^m NN0 ) )
4 coeeu.4 
 |-  ( ph -> M e. NN0 )
5 coeeu.5 
 |-  ( ph -> N e. NN0 )
6 coeeu.6 
 |-  ( ph -> ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } )
7 coeeu.7 
 |-  ( ph -> ( B " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
8 coeeu.8 
 |-  ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) ) )
9 coeeu.9 
 |-  ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) ) )
10 ssidd 
 |-  ( ph -> CC C_ CC )
11 4 5 nn0addcld 
 |-  ( ph -> ( M + N ) e. NN0 )
12 subcl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x - y ) e. CC )
13 12 adantl 
 |-  ( ( ph /\ ( x e. CC /\ y e. CC ) ) -> ( x - y ) e. CC )
14 cnex 
 |-  CC e. _V
15 nn0ex 
 |-  NN0 e. _V
16 14 15 elmap 
 |-  ( A e. ( CC ^m NN0 ) <-> A : NN0 --> CC )
17 2 16 sylib 
 |-  ( ph -> A : NN0 --> CC )
18 14 15 elmap 
 |-  ( B e. ( CC ^m NN0 ) <-> B : NN0 --> CC )
19 3 18 sylib 
 |-  ( ph -> B : NN0 --> CC )
20 15 a1i 
 |-  ( ph -> NN0 e. _V )
21 inidm 
 |-  ( NN0 i^i NN0 ) = NN0
22 13 17 19 20 20 21 off 
 |-  ( ph -> ( A oF - B ) : NN0 --> CC )
23 14 15 elmap 
 |-  ( ( A oF - B ) e. ( CC ^m NN0 ) <-> ( A oF - B ) : NN0 --> CC )
24 22 23 sylibr 
 |-  ( ph -> ( A oF - B ) e. ( CC ^m NN0 ) )
25 0cn 
 |-  0 e. CC
26 snssi 
 |-  ( 0 e. CC -> { 0 } C_ CC )
27 25 26 ax-mp 
 |-  { 0 } C_ CC
28 ssequn2 
 |-  ( { 0 } C_ CC <-> ( CC u. { 0 } ) = CC )
29 27 28 mpbi 
 |-  ( CC u. { 0 } ) = CC
30 29 oveq1i 
 |-  ( ( CC u. { 0 } ) ^m NN0 ) = ( CC ^m NN0 )
31 24 30 eleqtrrdi 
 |-  ( ph -> ( A oF - B ) e. ( ( CC u. { 0 } ) ^m NN0 ) )
32 11 nn0red 
 |-  ( ph -> ( M + N ) e. RR )
33 nn0re 
 |-  ( k e. NN0 -> k e. RR )
34 ltnle 
 |-  ( ( ( M + N ) e. RR /\ k e. RR ) -> ( ( M + N ) < k <-> -. k <_ ( M + N ) ) )
35 32 33 34 syl2an 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( M + N ) < k <-> -. k <_ ( M + N ) ) )
36 17 ffnd 
 |-  ( ph -> A Fn NN0 )
37 19 ffnd 
 |-  ( ph -> B Fn NN0 )
38 eqidd 
 |-  ( ( ph /\ k e. NN0 ) -> ( A ` k ) = ( A ` k ) )
39 eqidd 
 |-  ( ( ph /\ k e. NN0 ) -> ( B ` k ) = ( B ` k ) )
40 36 37 20 20 21 38 39 ofval 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( A oF - B ) ` k ) = ( ( A ` k ) - ( B ` k ) ) )
41 40 adantrr 
 |-  ( ( ph /\ ( k e. NN0 /\ ( M + N ) < k ) ) -> ( ( A oF - B ) ` k ) = ( ( A ` k ) - ( B ` k ) ) )
42 4 nn0red 
 |-  ( ph -> M e. RR )
43 42 adantr 
 |-  ( ( ph /\ ( k e. NN0 /\ ( M + N ) < k ) ) -> M e. RR )
44 32 adantr 
 |-  ( ( ph /\ ( k e. NN0 /\ ( M + N ) < k ) ) -> ( M + N ) e. RR )
45 33 adantl 
 |-  ( ( ph /\ k e. NN0 ) -> k e. RR )
46 45 adantrr 
 |-  ( ( ph /\ ( k e. NN0 /\ ( M + N ) < k ) ) -> k e. RR )
47 4 nn0cnd 
 |-  ( ph -> M e. CC )
48 5 nn0cnd 
 |-  ( ph -> N e. CC )
49 47 48 addcomd 
 |-  ( ph -> ( M + N ) = ( N + M ) )
50 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
51 5 50 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 0 ) )
52 4 nn0zd 
 |-  ( ph -> M e. ZZ )
53 eluzadd 
 |-  ( ( N e. ( ZZ>= ` 0 ) /\ M e. ZZ ) -> ( N + M ) e. ( ZZ>= ` ( 0 + M ) ) )
54 51 52 53 syl2anc 
 |-  ( ph -> ( N + M ) e. ( ZZ>= ` ( 0 + M ) ) )
55 49 54 eqeltrd 
 |-  ( ph -> ( M + N ) e. ( ZZ>= ` ( 0 + M ) ) )
56 47 addlidd 
 |-  ( ph -> ( 0 + M ) = M )
57 56 fveq2d 
 |-  ( ph -> ( ZZ>= ` ( 0 + M ) ) = ( ZZ>= ` M ) )
58 55 57 eleqtrd 
 |-  ( ph -> ( M + N ) e. ( ZZ>= ` M ) )
59 eluzle 
 |-  ( ( M + N ) e. ( ZZ>= ` M ) -> M <_ ( M + N ) )
60 58 59 syl 
 |-  ( ph -> M <_ ( M + N ) )
61 60 adantr 
 |-  ( ( ph /\ ( k e. NN0 /\ ( M + N ) < k ) ) -> M <_ ( M + N ) )
62 simprr 
 |-  ( ( ph /\ ( k e. NN0 /\ ( M + N ) < k ) ) -> ( M + N ) < k )
63 43 44 46 61 62 lelttrd 
 |-  ( ( ph /\ ( k e. NN0 /\ ( M + N ) < k ) ) -> M < k )
64 43 46 ltnled 
 |-  ( ( ph /\ ( k e. NN0 /\ ( M + N ) < k ) ) -> ( M < k <-> -. k <_ M ) )
65 63 64 mpbid 
 |-  ( ( ph /\ ( k e. NN0 /\ ( M + N ) < k ) ) -> -. k <_ M )
66 plyco0 
 |-  ( ( M e. NN0 /\ A : NN0 --> CC ) -> ( ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ M ) ) )
67 4 17 66 syl2anc 
 |-  ( ph -> ( ( A " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ M ) ) )
68 6 67 mpbid 
 |-  ( ph -> A. k e. NN0 ( ( A ` k ) =/= 0 -> k <_ M ) )
69 68 r19.21bi 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( A ` k ) =/= 0 -> k <_ M ) )
70 69 adantrr 
 |-  ( ( ph /\ ( k e. NN0 /\ ( M + N ) < k ) ) -> ( ( A ` k ) =/= 0 -> k <_ M ) )
71 70 necon1bd 
 |-  ( ( ph /\ ( k e. NN0 /\ ( M + N ) < k ) ) -> ( -. k <_ M -> ( A ` k ) = 0 ) )
72 65 71 mpd 
 |-  ( ( ph /\ ( k e. NN0 /\ ( M + N ) < k ) ) -> ( A ` k ) = 0 )
73 5 nn0red 
 |-  ( ph -> N e. RR )
74 73 adantr 
 |-  ( ( ph /\ ( k e. NN0 /\ ( M + N ) < k ) ) -> N e. RR )
75 4 50 eleqtrdi 
 |-  ( ph -> M e. ( ZZ>= ` 0 ) )
76 5 nn0zd 
 |-  ( ph -> N e. ZZ )
77 eluzadd 
 |-  ( ( M e. ( ZZ>= ` 0 ) /\ N e. ZZ ) -> ( M + N ) e. ( ZZ>= ` ( 0 + N ) ) )
78 75 76 77 syl2anc 
 |-  ( ph -> ( M + N ) e. ( ZZ>= ` ( 0 + N ) ) )
79 48 addlidd 
 |-  ( ph -> ( 0 + N ) = N )
80 79 fveq2d 
 |-  ( ph -> ( ZZ>= ` ( 0 + N ) ) = ( ZZ>= ` N ) )
81 78 80 eleqtrd 
 |-  ( ph -> ( M + N ) e. ( ZZ>= ` N ) )
82 eluzle 
 |-  ( ( M + N ) e. ( ZZ>= ` N ) -> N <_ ( M + N ) )
83 81 82 syl 
 |-  ( ph -> N <_ ( M + N ) )
84 83 adantr 
 |-  ( ( ph /\ ( k e. NN0 /\ ( M + N ) < k ) ) -> N <_ ( M + N ) )
85 74 44 46 84 62 lelttrd 
 |-  ( ( ph /\ ( k e. NN0 /\ ( M + N ) < k ) ) -> N < k )
86 74 46 ltnled 
 |-  ( ( ph /\ ( k e. NN0 /\ ( M + N ) < k ) ) -> ( N < k <-> -. k <_ N ) )
87 85 86 mpbid 
 |-  ( ( ph /\ ( k e. NN0 /\ ( M + N ) < k ) ) -> -. k <_ N )
88 plyco0 
 |-  ( ( N e. NN0 /\ B : NN0 --> CC ) -> ( ( B " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( B ` k ) =/= 0 -> k <_ N ) ) )
89 5 19 88 syl2anc 
 |-  ( ph -> ( ( B " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( B ` k ) =/= 0 -> k <_ N ) ) )
90 7 89 mpbid 
 |-  ( ph -> A. k e. NN0 ( ( B ` k ) =/= 0 -> k <_ N ) )
91 90 r19.21bi 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( B ` k ) =/= 0 -> k <_ N ) )
92 91 adantrr 
 |-  ( ( ph /\ ( k e. NN0 /\ ( M + N ) < k ) ) -> ( ( B ` k ) =/= 0 -> k <_ N ) )
93 92 necon1bd 
 |-  ( ( ph /\ ( k e. NN0 /\ ( M + N ) < k ) ) -> ( -. k <_ N -> ( B ` k ) = 0 ) )
94 87 93 mpd 
 |-  ( ( ph /\ ( k e. NN0 /\ ( M + N ) < k ) ) -> ( B ` k ) = 0 )
95 72 94 oveq12d 
 |-  ( ( ph /\ ( k e. NN0 /\ ( M + N ) < k ) ) -> ( ( A ` k ) - ( B ` k ) ) = ( 0 - 0 ) )
96 0m0e0 
 |-  ( 0 - 0 ) = 0
97 95 96 eqtrdi 
 |-  ( ( ph /\ ( k e. NN0 /\ ( M + N ) < k ) ) -> ( ( A ` k ) - ( B ` k ) ) = 0 )
98 41 97 eqtrd 
 |-  ( ( ph /\ ( k e. NN0 /\ ( M + N ) < k ) ) -> ( ( A oF - B ) ` k ) = 0 )
99 98 expr 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( M + N ) < k -> ( ( A oF - B ) ` k ) = 0 ) )
100 35 99 sylbird 
 |-  ( ( ph /\ k e. NN0 ) -> ( -. k <_ ( M + N ) -> ( ( A oF - B ) ` k ) = 0 ) )
101 100 necon1ad 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( ( A oF - B ) ` k ) =/= 0 -> k <_ ( M + N ) ) )
102 101 ralrimiva 
 |-  ( ph -> A. k e. NN0 ( ( ( A oF - B ) ` k ) =/= 0 -> k <_ ( M + N ) ) )
103 plyco0 
 |-  ( ( ( M + N ) e. NN0 /\ ( A oF - B ) : NN0 --> CC ) -> ( ( ( A oF - B ) " ( ZZ>= ` ( ( M + N ) + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( ( A oF - B ) ` k ) =/= 0 -> k <_ ( M + N ) ) ) )
104 11 22 103 syl2anc 
 |-  ( ph -> ( ( ( A oF - B ) " ( ZZ>= ` ( ( M + N ) + 1 ) ) ) = { 0 } <-> A. k e. NN0 ( ( ( A oF - B ) ` k ) =/= 0 -> k <_ ( M + N ) ) ) )
105 102 104 mpbird 
 |-  ( ph -> ( ( A oF - B ) " ( ZZ>= ` ( ( M + N ) + 1 ) ) ) = { 0 } )
106 df-0p 
 |-  0p = ( CC X. { 0 } )
107 fconstmpt 
 |-  ( CC X. { 0 } ) = ( z e. CC |-> 0 )
108 106 107 eqtri 
 |-  0p = ( z e. CC |-> 0 )
109 elfznn0 
 |-  ( k e. ( 0 ... ( M + N ) ) -> k e. NN0 )
110 40 adantlr 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. NN0 ) -> ( ( A oF - B ) ` k ) = ( ( A ` k ) - ( B ` k ) ) )
111 110 oveq1d 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. NN0 ) -> ( ( ( A oF - B ) ` k ) x. ( z ^ k ) ) = ( ( ( A ` k ) - ( B ` k ) ) x. ( z ^ k ) ) )
112 17 adantr 
 |-  ( ( ph /\ z e. CC ) -> A : NN0 --> CC )
113 112 ffvelcdmda 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. NN0 ) -> ( A ` k ) e. CC )
114 19 adantr 
 |-  ( ( ph /\ z e. CC ) -> B : NN0 --> CC )
115 114 ffvelcdmda 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. NN0 ) -> ( B ` k ) e. CC )
116 expcl 
 |-  ( ( z e. CC /\ k e. NN0 ) -> ( z ^ k ) e. CC )
117 116 adantll 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. NN0 ) -> ( z ^ k ) e. CC )
118 113 115 117 subdird 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. NN0 ) -> ( ( ( A ` k ) - ( B ` k ) ) x. ( z ^ k ) ) = ( ( ( A ` k ) x. ( z ^ k ) ) - ( ( B ` k ) x. ( z ^ k ) ) ) )
119 111 118 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 ) ) ) )
120 109 119 sylan2 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... ( M + N ) ) ) -> ( ( ( A oF - B ) ` k ) x. ( z ^ k ) ) = ( ( ( A ` k ) x. ( z ^ k ) ) - ( ( B ` k ) x. ( z ^ k ) ) ) )
121 120 sumeq2dv 
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 0 ... ( M + N ) ) ( ( ( A oF - B ) ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... ( M + N ) ) ( ( ( A ` k ) x. ( z ^ k ) ) - ( ( B ` k ) x. ( z ^ k ) ) ) )
122 fzfid 
 |-  ( ( ph /\ z e. CC ) -> ( 0 ... ( M + N ) ) e. Fin )
123 113 117 mulcld 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. NN0 ) -> ( ( A ` k ) x. ( z ^ k ) ) e. CC )
124 109 123 sylan2 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... ( M + N ) ) ) -> ( ( A ` k ) x. ( z ^ k ) ) e. CC )
125 115 117 mulcld 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. NN0 ) -> ( ( B ` k ) x. ( z ^ k ) ) e. CC )
126 109 125 sylan2 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... ( M + N ) ) ) -> ( ( B ` k ) x. ( z ^ k ) ) e. CC )
127 122 124 126 fsumsub 
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 0 ... ( M + N ) ) ( ( ( A ` k ) x. ( z ^ k ) ) - ( ( B ` k ) x. ( z ^ k ) ) ) = ( sum_ k e. ( 0 ... ( M + N ) ) ( ( A ` k ) x. ( z ^ k ) ) - sum_ k e. ( 0 ... ( M + N ) ) ( ( B ` k ) x. ( z ^ k ) ) ) )
128 122 124 fsumcl 
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 0 ... ( M + N ) ) ( ( A ` k ) x. ( z ^ k ) ) e. CC )
129 8 9 eqtr3d 
 |-  ( ph -> ( z e. CC |-> sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) ) )
130 129 fveq1d 
 |-  ( ph -> ( ( z e. CC |-> sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) ) ` z ) = ( ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) ) ` z ) )
131 130 adantr 
 |-  ( ( ph /\ z e. CC ) -> ( ( z e. CC |-> sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) ) ` z ) = ( ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) ) ` z ) )
132 simpr 
 |-  ( ( ph /\ z e. CC ) -> z e. CC )
133 sumex 
 |-  sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) e. _V
134 eqid 
 |-  ( z e. CC |-> sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) )
135 134 fvmpt2 
 |-  ( ( z e. CC /\ sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) e. _V ) -> ( ( z e. CC |-> sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) ) ` z ) = sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) )
136 132 133 135 sylancl 
 |-  ( ( ph /\ z e. CC ) -> ( ( z e. CC |-> sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) ) ` z ) = sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) )
137 fzss2 
 |-  ( ( M + N ) e. ( ZZ>= ` M ) -> ( 0 ... M ) C_ ( 0 ... ( M + N ) ) )
138 58 137 syl 
 |-  ( ph -> ( 0 ... M ) C_ ( 0 ... ( M + N ) ) )
139 138 adantr 
 |-  ( ( ph /\ z e. CC ) -> ( 0 ... M ) C_ ( 0 ... ( M + N ) ) )
140 139 sselda 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> k e. ( 0 ... ( M + N ) ) )
141 140 124 syldan 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... M ) ) -> ( ( A ` k ) x. ( z ^ k ) ) e. CC )
142 eldifn 
 |-  ( k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) -> -. k e. ( 0 ... M ) )
143 142 adantl 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> -. k e. ( 0 ... M ) )
144 eldifi 
 |-  ( k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) -> k e. ( 0 ... ( M + N ) ) )
145 144 109 syl 
 |-  ( k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) -> k e. NN0 )
146 simpr 
 |-  ( ( ph /\ k e. NN0 ) -> k e. NN0 )
147 146 50 eleqtrdi 
 |-  ( ( ph /\ k e. NN0 ) -> k e. ( ZZ>= ` 0 ) )
148 52 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> M e. ZZ )
149 elfz5 
 |-  ( ( k e. ( ZZ>= ` 0 ) /\ M e. ZZ ) -> ( k e. ( 0 ... M ) <-> k <_ M ) )
150 147 148 149 syl2anc 
 |-  ( ( ph /\ k e. NN0 ) -> ( k e. ( 0 ... M ) <-> k <_ M ) )
151 69 150 sylibrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( A ` k ) =/= 0 -> k e. ( 0 ... M ) ) )
152 151 adantlr 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. NN0 ) -> ( ( A ` k ) =/= 0 -> k e. ( 0 ... M ) ) )
153 152 necon1bd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. NN0 ) -> ( -. k e. ( 0 ... M ) -> ( A ` k ) = 0 ) )
154 145 153 sylan2 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> ( -. k e. ( 0 ... M ) -> ( A ` k ) = 0 ) )
155 143 154 mpd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> ( A ` k ) = 0 )
156 155 oveq1d 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> ( ( A ` k ) x. ( z ^ k ) ) = ( 0 x. ( z ^ k ) ) )
157 132 145 116 syl2an 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> ( z ^ k ) e. CC )
158 157 mul02d 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> ( 0 x. ( z ^ k ) ) = 0 )
159 156 158 eqtrd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... M ) ) ) -> ( ( A ` k ) x. ( z ^ k ) ) = 0 )
160 139 141 159 122 fsumss 
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... ( M + N ) ) ( ( A ` k ) x. ( z ^ k ) ) )
161 136 160 eqtrd 
 |-  ( ( ph /\ z e. CC ) -> ( ( z e. CC |-> sum_ k e. ( 0 ... M ) ( ( A ` k ) x. ( z ^ k ) ) ) ` z ) = sum_ k e. ( 0 ... ( M + N ) ) ( ( A ` k ) x. ( z ^ k ) ) )
162 sumex 
 |-  sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) e. _V
163 eqid 
 |-  ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) )
164 163 fvmpt2 
 |-  ( ( z e. CC /\ sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) e. _V ) -> ( ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) ) ` z ) = sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) )
165 132 162 164 sylancl 
 |-  ( ( ph /\ z e. CC ) -> ( ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) ) ` z ) = sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) )
166 fzss2 
 |-  ( ( M + N ) e. ( ZZ>= ` N ) -> ( 0 ... N ) C_ ( 0 ... ( M + N ) ) )
167 81 166 syl 
 |-  ( ph -> ( 0 ... N ) C_ ( 0 ... ( M + N ) ) )
168 167 adantr 
 |-  ( ( ph /\ z e. CC ) -> ( 0 ... N ) C_ ( 0 ... ( M + N ) ) )
169 168 sselda 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... N ) ) -> k e. ( 0 ... ( M + N ) ) )
170 169 126 syldan 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... N ) ) -> ( ( B ` k ) x. ( z ^ k ) ) e. CC )
171 eldifn 
 |-  ( k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... N ) ) -> -. k e. ( 0 ... N ) )
172 171 adantl 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... N ) ) ) -> -. k e. ( 0 ... N ) )
173 eldifi 
 |-  ( k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... N ) ) -> k e. ( 0 ... ( M + N ) ) )
174 173 109 syl 
 |-  ( k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... N ) ) -> k e. NN0 )
175 76 adantr 
 |-  ( ( ph /\ k e. NN0 ) -> N e. ZZ )
176 elfz5 
 |-  ( ( k e. ( ZZ>= ` 0 ) /\ N e. ZZ ) -> ( k e. ( 0 ... N ) <-> k <_ N ) )
177 147 175 176 syl2anc 
 |-  ( ( ph /\ k e. NN0 ) -> ( k e. ( 0 ... N ) <-> k <_ N ) )
178 91 177 sylibrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( B ` k ) =/= 0 -> k e. ( 0 ... N ) ) )
179 178 adantlr 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. NN0 ) -> ( ( B ` k ) =/= 0 -> k e. ( 0 ... N ) ) )
180 179 necon1bd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. NN0 ) -> ( -. k e. ( 0 ... N ) -> ( B ` k ) = 0 ) )
181 174 180 sylan2 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... N ) ) ) -> ( -. k e. ( 0 ... N ) -> ( B ` k ) = 0 ) )
182 172 181 mpd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... N ) ) ) -> ( B ` k ) = 0 )
183 182 oveq1d 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... N ) ) ) -> ( ( B ` k ) x. ( z ^ k ) ) = ( 0 x. ( z ^ k ) ) )
184 132 174 116 syl2an 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... N ) ) ) -> ( z ^ k ) e. CC )
185 184 mul02d 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... N ) ) ) -> ( 0 x. ( z ^ k ) ) = 0 )
186 183 185 eqtrd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( ( 0 ... ( M + N ) ) \ ( 0 ... N ) ) ) -> ( ( B ` k ) x. ( z ^ k ) ) = 0 )
187 168 170 186 122 fsumss 
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... ( M + N ) ) ( ( B ` k ) x. ( z ^ k ) ) )
188 165 187 eqtrd 
 |-  ( ( ph /\ z e. CC ) -> ( ( z e. CC |-> sum_ k e. ( 0 ... N ) ( ( B ` k ) x. ( z ^ k ) ) ) ` z ) = sum_ k e. ( 0 ... ( M + N ) ) ( ( B ` k ) x. ( z ^ k ) ) )
189 131 161 188 3eqtr3d 
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 0 ... ( M + N ) ) ( ( A ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... ( M + N ) ) ( ( B ` k ) x. ( z ^ k ) ) )
190 128 189 subeq0bd 
 |-  ( ( ph /\ z e. CC ) -> ( sum_ k e. ( 0 ... ( M + N ) ) ( ( A ` k ) x. ( z ^ k ) ) - sum_ k e. ( 0 ... ( M + N ) ) ( ( B ` k ) x. ( z ^ k ) ) ) = 0 )
191 121 127 190 3eqtrrd 
 |-  ( ( ph /\ z e. CC ) -> 0 = sum_ k e. ( 0 ... ( M + N ) ) ( ( ( A oF - B ) ` k ) x. ( z ^ k ) ) )
192 191 mpteq2dva 
 |-  ( ph -> ( z e. CC |-> 0 ) = ( z e. CC |-> sum_ k e. ( 0 ... ( M + N ) ) ( ( ( A oF - B ) ` k ) x. ( z ^ k ) ) ) )
193 108 192 eqtrid 
 |-  ( ph -> 0p = ( z e. CC |-> sum_ k e. ( 0 ... ( M + N ) ) ( ( ( A oF - B ) ` k ) x. ( z ^ k ) ) ) )
194 10 11 31 105 193 plyeq0 
 |-  ( ph -> ( A oF - B ) = ( NN0 X. { 0 } ) )
195 ofsubeq0 
 |-  ( ( NN0 e. _V /\ A : NN0 --> CC /\ B : NN0 --> CC ) -> ( ( A oF - B ) = ( NN0 X. { 0 } ) <-> A = B ) )
196 15 17 19 195 mp3an2i 
 |-  ( ph -> ( ( A oF - B ) = ( NN0 X. { 0 } ) <-> A = B ) )
197 194 196 mpbid 
 |-  ( ph -> A = B )