Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  vieta1lem2 Structured version   Visualization version   Unicode version

Theorem vieta1lem2 23343
 Description: Lemma for vieta1 23344: inductive step. Let be a root of . Then for some by the factor theorem, and is a degree- polynomial, so by the induction hypothesis coeff coeff, so coeff coeff. Now the coefficients of are coeff and coeff coeff , which works out to coeff coeff , so putting it all together we have as we wanted to show. (Contributed by Mario Carneiro, 28-Jul-2014.)
Hypotheses
Ref Expression
vieta1.1 coeff
vieta1.2 deg
vieta1.3
vieta1.4 Poly
vieta1.5
vieta1lem.6
vieta1lem.7
vieta1lem.8 Poly deg deg coeffdeg coeffdeg
vieta1lem.9 quot
Assertion
Ref Expression
vieta1lem2
Distinct variable groups:   ,   ,   ,,   ,,   ,   ,,   ,,   ,,
Allowed substitution hints:   ()   ()   (,)   ()   (,,)   (,)   ()

Proof of Theorem vieta1lem2
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 vieta1.5 . . . . 5
2 vieta1lem.7 . . . . . . 7
3 vieta1lem.6 . . . . . . . 8
43peano2nnd 10648 . . . . . . 7
52, 4eqeltrrd 2550 . . . . . 6
65nnne0d 10676 . . . . 5
71, 6eqnetrd 2710 . . . 4
8 vieta1.4 . . . . . . . 8 Poly
9 vieta1.2 . . . . . . . . . 10 deg
109, 6syl5eqner 2718 . . . . . . . . 9 deg
11 fveq2 5879 . . . . . . . . . . 11 deg deg
12 dgr0 23295 . . . . . . . . . . 11 deg
1311, 12syl6eq 2521 . . . . . . . . . 10 deg
1413necon3i 2675 . . . . . . . . 9 deg
1510, 14syl 17 . . . . . . . 8
16 vieta1.3 . . . . . . . . 9
1716fta1 23340 . . . . . . . 8 Poly deg
188, 15, 17syl2anc 673 . . . . . . 7 deg
1918simpld 466 . . . . . 6
20 hasheq0 12582 . . . . . 6
2119, 20syl 17 . . . . 5
2221necon3bid 2687 . . . 4
237, 22mpbid 215 . . 3
24 n0 3732 . . 3
2523, 24sylib 201 . 2
26 incom 3616 . . . . 5
27 vieta1.1 . . . . . . . . . . 11 coeff
28 vieta1lem.8 . . . . . . . . . . 11 Poly deg deg coeffdeg coeffdeg
29 vieta1lem.9 . . . . . . . . . . 11 quot
3027, 9, 16, 8, 1, 3, 2, 28, 29vieta1lem1 23342 . . . . . . . . . 10 Poly deg
3130simprd 470 . . . . . . . . 9 deg
3230simpld 466 . . . . . . . . . . 11 Poly
33 dgrcl 23266 . . . . . . . . . . 11 Poly deg
3432, 33syl 17 . . . . . . . . . 10 deg
3534nn0red 10950 . . . . . . . . 9 deg
3631, 35eqeltrd 2549 . . . . . . . 8
3736ltp1d 10559 . . . . . . . 8
3836, 37gtned 9787 . . . . . . 7
39 snssi 4107 . . . . . . . . . . 11
40 ssequn1 3595 . . . . . . . . . . 11
4139, 40sylib 201 . . . . . . . . . 10
4241fveq2d 5883 . . . . . . . . 9
438adantr 472 . . . . . . . . . . . . . . . . . 18 Poly
44 cnvimass 5194 . . . . . . . . . . . . . . . . . . . . 21
4516, 44eqsstri 3448 . . . . . . . . . . . . . . . . . . . 20
46 plyf 23231 . . . . . . . . . . . . . . . . . . . . 21 Poly
47 fdm 5745 . . . . . . . . . . . . . . . . . . . . 21
488, 46, 473syl 18 . . . . . . . . . . . . . . . . . . . 20
4945, 48syl5sseq 3466 . . . . . . . . . . . . . . . . . . 19
5049sselda 3418 . . . . . . . . . . . . . . . . . 18
5116eleq2i 2541 . . . . . . . . . . . . . . . . . . . 20
52 ffn 5739 . . . . . . . . . . . . . . . . . . . . 21
53 fniniseg 6018 . . . . . . . . . . . . . . . . . . . . 21
548, 46, 52, 534syl 19 . . . . . . . . . . . . . . . . . . . 20
5551, 54syl5bb 265 . . . . . . . . . . . . . . . . . . 19
5655simplbda 636 . . . . . . . . . . . . . . . . . 18
57 eqid 2471 . . . . . . . . . . . . . . . . . . 19
5857facth 23338 . . . . . . . . . . . . . . . . . 18 Poly quot
5943, 50, 56, 58syl3anc 1292 . . . . . . . . . . . . . . . . 17 quot
6029oveq2i 6319 . . . . . . . . . . . . . . . . 17 quot
6159, 60syl6eqr 2523 . . . . . . . . . . . . . . . 16
6261cnveqd 5015 . . . . . . . . . . . . . . 15
6362imaeq1d 5173 . . . . . . . . . . . . . 14
6416, 63syl5eq 2517 . . . . . . . . . . . . 13
65 cnex 9638 . . . . . . . . . . . . . . 15
6665a1i 11 . . . . . . . . . . . . . 14
6757plyremlem 23336 . . . . . . . . . . . . . . . . 17 Poly deg
6850, 67syl 17 . . . . . . . . . . . . . . . 16 Poly deg
6968simp1d 1042 . . . . . . . . . . . . . . 15 Poly
70 plyf 23231 . . . . . . . . . . . . . . 15 Poly
7169, 70syl 17 . . . . . . . . . . . . . 14
72 plyf 23231 . . . . . . . . . . . . . . 15 Poly
7332, 72syl 17 . . . . . . . . . . . . . 14
74 ofmulrt 23314 . . . . . . . . . . . . . 14
7566, 71, 73, 74syl3anc 1292 . . . . . . . . . . . . 13
7668simp3d 1044 . . . . . . . . . . . . . 14
7776uneq1d 3578 . . . . . . . . . . . . 13
7864, 75, 773eqtrd 2509 . . . . . . . . . . . 12
7978fveq2d 5883 . . . . . . . . . . 11
801, 2eqtr4d 2508 . . . . . . . . . . . 12
8180adantr 472 . . . . . . . . . . 11
8279, 81eqtr3d 2507 . . . . . . . . . 10
8315adantr 472 . . . . . . . . . . . . . . . . . 18
8461, 83eqnetrrd 2711 . . . . . . . . . . . . . . . . 17
85 plymul0or 23313 . . . . . . . . . . . . . . . . . . 19 Poly Poly
8669, 32, 85syl2anc 673 . . . . . . . . . . . . . . . . . 18
8786necon3abid 2679 . . . . . . . . . . . . . . . . 17
8884, 87mpbid 215 . . . . . . . . . . . . . . . 16
89 neanior 2735 . . . . . . . . . . . . . . . 16
9088, 89sylibr 217 . . . . . . . . . . . . . . 15
9190simprd 470 . . . . . . . . . . . . . 14
92 eqid 2471 . . . . . . . . . . . . . . 15
9392fta1 23340 . . . . . . . . . . . . . 14 Poly deg
9432, 91, 93syl2anc 673 . . . . . . . . . . . . 13 deg
9594simprd 470 . . . . . . . . . . . 12 deg
9695, 31breqtrrd 4422 . . . . . . . . . . 11
97 snfi 7668 . . . . . . . . . . . . . 14
9894simpld 466 . . . . . . . . . . . . . 14
99 hashun2 12600 . . . . . . . . . . . . . 14
10097, 98, 99sylancr 676 . . . . . . . . . . . . 13
101 ax-1cn 9615 . . . . . . . . . . . . . . 15
1023nncnd 10647 . . . . . . . . . . . . . . . 16
103102adantr 472 . . . . . . . . . . . . . . 15
104 addcom 9837 . . . . . . . . . . . . . . 15
105101, 103, 104sylancr 676 . . . . . . . . . . . . . 14
10682, 105eqtr4d 2508 . . . . . . . . . . . . 13
107 hashsng 12587 . . . . . . . . . . . . . . 15
108107adantl 473 . . . . . . . . . . . . . 14
109108oveq1d 6323 . . . . . . . . . . . . 13
110100, 106, 1093brtr3d 4425 . . . . . . . . . . . 12
111 hashcl 12576 . . . . . . . . . . . . . . 15
11298, 111syl 17 . . . . . . . . . . . . . 14
113112nn0red 10950 . . . . . . . . . . . . 13
114 1red 9676 . . . . . . . . . . . . 13
11536, 113, 114leadd2d 10229 . . . . . . . . . . . 12
116110, 115mpbird 240 . . . . . . . . . . 11
117113, 36letri3d 9794 . . . . . . . . . . 11
11896, 116, 117mpbir2and 936 . . . . . . . . . 10
11982, 118eqeq12d 2486 . . . . . . . . 9
12042, 119syl5ib 227 . . . . . . . 8
121120necon3ad 2656 . . . . . . 7
12238, 121mpd 15 . . . . . 6
123 disjsn 4023 . . . . . 6
124122, 123sylibr 217 . . . . 5
12526, 124syl5eq 2517 . . . 4
12619adantr 472 . . . 4
12749adantr 472 . . . . 5
128127sselda 3418 . . . 4
129125, 78, 126, 128fsumsplit 13883 . . 3
130 id 22 . . . . . . 7
131130sumsn 13884 . . . . . 6
13250, 50, 131syl2anc 673 . . . . 5
13350negnegd 9996 . . . . 5
134132, 133eqtr4d 2508 . . . 4
135118, 31eqtrd 2505 . . . . . 6 deg
13628adantr 472 . . . . . . 7 Poly deg deg coeffdeg coeffdeg
137 fveq2 5879 . . . . . . . . . . 11 deg deg
138137eqeq2d 2481 . . . . . . . . . 10 deg deg
139 cnveq 5013 . . . . . . . . . . . . 13
140139imaeq1d 5173 . . . . . . . . . . . 12
141140fveq2d 5883 . . . . . . . . . . 11
142141, 137eqeq12d 2486 . . . . . . . . . 10 deg deg
143138, 142anbi12d 725 . . . . . . . . 9 deg deg deg deg
144140sumeq1d 13844 . . . . . . . . . 10
145 fveq2 5879 . . . . . . . . . . . . 13 coeff coeff
146137oveq1d 6323 . . . . . . . . . . . . 13 deg deg
147145, 146fveq12d 5885 . . . . . . . . . . . 12 coeffdeg coeffdeg
148145, 137fveq12d 5885 . . . . . . . . . . . 12 coeffdeg coeffdeg
149147, 148oveq12d 6326 . . . . . . . . . . 11 coeffdeg coeffdeg coeffdeg coeffdeg
150149negeqd 9889 . . . . . . . . . 10 coeffdeg coeffdeg coeffdeg coeffdeg
151144, 150eqeq12d 2486 . . . . . . . . 9 coeffdeg coeffdeg coeffdeg coeffdeg
152143, 151imbi12d 327 . . . . . . . 8 deg deg coeffdeg coeffdeg deg deg coeffdeg coeffdeg
153152rspcv 3132 . . . . . . 7 Poly Poly deg deg coeffdeg coeffdeg deg deg coeffdeg coeffdeg
15432, 136, 153sylc 61 . . . . . 6 deg deg coeffdeg coeffdeg
15531, 135, 154mp2and 693 . . . . 5 coeffdeg coeffdeg
15631oveq1d 6323 . . . . . . . 8 deg
157156fveq2d 5883 . . . . . . 7 coeff coeffdeg
15861fveq2d 5883 . . . . . . . . . 10 coeff coeff
15927, 158syl5eq 2517 . . . . . . . . 9 coeff
16061fveq2d 5883 . . . . . . . . . . 11 deg deg
16168simp2d 1043 . . . . . . . . . . . . . 14 deg
162 ax-1ne0 9626 . . . . . . . . . . . . . . 15
163162a1i 11 . . . . . . . . . . . . . 14
164161, 163eqnetrd 2710 . . . . . . . . . . . . 13 deg
165 fveq2 5879 . . . . . . . . . . . . . . 15 deg deg
166165, 12syl6eq 2521 . . . . . . . . . . . . . 14 deg
167166necon3i 2675 . . . . . . . . . . . . 13 deg
168164, 167syl 17 . . . . . . . . . . . 12
169 eqid 2471 . . . . . . . . . . . . 13 deg deg
170 eqid 2471 . . . . . . . . . . . . 13 deg deg
171169, 170dgrmul 23303 . . . . . . . . . . . 12 Poly Poly deg deg deg
17269, 168, 32, 91, 171syl22anc 1293 . . . . . . . . . . 11 deg deg deg
173160, 172eqtrd 2505 . . . . . . . . . 10 deg deg deg
1749, 173syl5eq 2517 . . . . . . . . 9 deg deg
175159, 174fveq12d 5885 . . . . . . . 8 coeff deg deg
176 eqid 2471 . . . . . . . . . 10 coeff coeff
177 eqid 2471 . . . . . . . . . 10 coeff coeff
178176, 177, 169, 170coemulhi 23287 . . . . . . . . 9 Poly Poly coeff deg deg coeff deg coeffdeg
17969, 32, 178syl2anc 673 . . . . . . . 8 coeff deg deg coeff deg coeffdeg
180161fveq2d 5883 . . . . . . . . . . 11 coeff deg coeff
181 ssid 3437 . . . . . . . . . . . . . . 15
182 plyid 23242 . . . . . . . . . . . . . . 15 Poly
183181, 101, 182mp2an 686 . . . . . . . . . . . . . 14 Poly
184 plyconst 23239 . . . . . . . . . . . . . . 15 Poly
185181, 50, 184sylancr 676 . . . . . . . . . . . . . 14 Poly
186 eqid 2471 . . . . . . . . . . . . . . 15 coeff coeff
187 eqid 2471 . . . . . . . . . . . . . . 15 coeff coeff
188186, 187coesub 23290 . . . . . . . . . . . . . 14 Poly Poly coeff coeff coeff
189183, 185, 188sylancr 676 . . . . . . . . . . . . 13 coeff coeff coeff
190189fveq1d 5881 . . . . . . . . . . . 12 coeff coeff coeff
191 1nn0 10909 . . . . . . . . . . . . . 14
192186coef3 23265 . . . . . . . . . . . . . . . . 17 Poly coeff
193 ffn 5739 . . . . . . . . . . . . . . . . 17 coeff coeff
194183, 192, 193mp2b 10 . . . . . . . . . . . . . . . 16 coeff
195194a1i 11 . . . . . . . . . . . . . . 15 coeff
196187coef3 23265 . . . . . . . . . . . . . . . 16 Poly coeff
197 ffn 5739 . . . . . . . . . . . . . . . 16 coeff coeff
198185, 196, 1973syl 18 . . . . . . . . . . . . . . 15 coeff
199 nn0ex 10899 . . . . . . . . . . . . . . . 16
200199a1i 11 . . . . . . . . . . . . . . 15
201 inidm 3632 . . . . . . . . . . . . . . 15
202 coeidp 23296 . . . . . . . . . . . . . . . . 17 coeff
203202adantl 473 . . . . . . . . . . . . . . . 16 coeff
204 eqid 2471 . . . . . . . . . . . . . . . . 17
205204iftruei 3879 . . . . . . . . . . . . . . . 16
206203, 205syl6eq 2521 . . . . . . . . . . . . . . 15 coeff
207 0lt1 10157 . . . . . . . . . . . . . . . . . 18
208 0re 9661 . . . . . . . . . . . . . . . . . . 19
209 1re 9660 . . . . . . . . . . . . . . . . . . 19
210208, 209ltnlei 9773 . . . . . . . . . . . . . . . . . 18
211207, 210mpbi 213 . . . . . . . . . . . . . . . . 17
21250adantr 472 . . . . . . . . . . . . . . . . . . 19
213 0dgr 23278 . . . . . . . . . . . . . . . . . . 19 deg
214212, 213syl 17 . . . . . . . . . . . . . . . . . 18 deg
215214breq2d 4407 . . . . . . . . . . . . . . . . 17 deg
216211, 215mtbiri 310 . . . . . . . . . . . . . . . 16 deg
217 eqid 2471 . . . . . . . . . . . . . . . . . . . 20 deg deg
218187, 217dgrub 23267 . . . . . . . . . . . . . . . . . . 19 Poly coeff deg
2192183expia 1233 . . . . . . . . . . . . . . . . . 18 Poly coeff deg
220185, 219sylan 479 . . . . . . . . . . . . . . . . 17 coeff deg
221220necon1bd 2661 . . . . . . . . . . . . . . . 16 deg coeff
222216, 221mpd 15 . . . . . . . . . . . . . . 15 coeff
223195, 198, 200, 200, 201, 206, 222ofval 6559 . . . . . . . . . . . . . 14 coeff coeff
224191, 223mpan2 685 . . . . . . . . . . . . 13 coeff coeff
225 1m0e1 10742 . . . . . . . . . . . . 13
226224, 225syl6eq 2521 . . . . . . . . . . . 12 coeff coeff
227190, 226eqtrd 2505 . . . . . . . . . . 11 coeff
228180, 227eqtrd 2505 . . . . . . . . . 10 coeff deg
229228oveq1d 6323 . . . . . . . . 9 coeff deg coeffdeg coeffdeg
230177coef3 23265 . . . . . . . . . . . 12 Poly coeff
23132, 230syl 17 . . . . . . . . . . 11 coeff
232231, 34ffvelrnd 6038 . . . . . . . . . 10 coeffdeg
233232mulid2d 9679 . . . . . . . . 9 coeffdeg coeffdeg
234229, 233eqtrd 2505 . . . . . . . 8 coeff deg coeffdeg coeffdeg
235175, 179, 2343eqtrd 2509 . . . . . . 7 coeffdeg
236157, 235oveq12d 6326 . . . . . 6 coeff coeffdeg coeffdeg
237236negeqd 9889 . . . . 5 coeff coeffdeg coeffdeg
238155, 237eqtr4d 2508 . . . 4 coeff
239134, 238oveq12d 6326 . . 3 coeff
24050negcld 9992 . . . . 5
241 nnm1nn0 10935 . . . . . . . . 9
2423, 241syl 17 . . . . . . . 8
243242adantr 472 . . . . . . 7
244231, 243ffvelrnd 6038 . . . . . 6 coeff
245235, 232eqeltrd 2549 . . . . . 6
2469, 27dgreq0 23298 . . . . . . . . 9 Poly
24743, 246syl 17 . . . . . . . 8
248247necon3bid 2687 . . . . . . 7
24983, 248mpbid 215 . . . . . 6
250244, 245, 249divcld 10405 . . . . 5 coeff
251240, 250negdid 10018 . . . 4 coeff coeff
252240, 245mulcld 9681 . . . . . . 7
253252, 244, 245, 249divdird 10443 . . . . . 6 coeff coeff
254 nnm1nn0 10935 . . . . . . . . . . 11
2555, 254syl 17 . . . . . . . . . 10
256255adantr 472 . . . . . . . . 9
257176, 177coemul 23285 . . . . . . . . 9 Poly Poly coeff coeff coeff
25869, 32, 256, 257syl3anc 1292 . . . . . . . 8 coeff coeff coeff
259159fveq1d 5881 . . . . . . . 8 coeff
260 1e0p1 11102 . . . . . . . . . . . 12
261260oveq2i 6319 . . . . . . . . . . 11
262261sumeq1i 13841 . . . . . . . . . 10 coeff coeff coeff coeff
263 0nn0 10908 . . . . . . . . . . . . 13
264 nn0uz 11217 . . . . . . . . . . . . 13
265263, 264eleqtri 2547 . . . . . . . . . . . 12
266265a1i 11 . . . . . . . . . . 11
267261eleq2i 2541 . . . . . . . . . . . 12
268176coef3 23265 . . . . . . . . . . . . . . 15 Poly coeff
26969, 268syl 17 . . . . . . . . . . . . . 14 coeff
270 elfznn0 11913 . . . . . . . . . . . . . 14
271 ffvelrn 6035 . . . . . . . . . . . . . 14 coeff coeff
272269, 270, 271syl2an 485 . . . . . . . . . . . . 13 coeff
2732oveq1d 6323 . . . . . . . . . . . . . . . . . . . 20
274 pncan 9901 . . . . . . . . . . . . . . . . . . . . 21
275102, 101, 274sylancl 675 . . . . . . . . . . . . . . . . . . . 20
276273, 275eqtr3d 2507 . . . . . . . . . . . . . . . . . . 19
277276adantr 472 . . . . . . . . . . . . . . . . . 18
2783adantr 472 . . . . . . . . . . . . . . . . . 18
279277, 278eqeltrd 2549 . . . . . . . . . . . . . . . . 17
280 nnuz 11218 . . . . . . . . . . . . . . . . 17
281279, 280syl6eleq 2559 . . . . . . . . . . . . . . . 16
282 fzss2 11864 . . . . . . . . . . . . . . . 16
283281, 282syl 17 . . . . . . . . . . . . . . 15
284283sselda 3418 . . . . . . . . . . . . . 14
285 fznn0sub 11857 . . . . . . . . . . . . . . 15
286 ffvelrn 6035 . . . . . . . . . . . . . . 15 coeff coeff
287231, 285, 286syl2an 485 . . . . . . . . . . . . . 14 coeff
288284, 287syldan 478 . . . . . . . . . . . . 13 coeff
289272, 288mulcld 9681 . . . . . . . . . . . 12 coeff coeff
290267, 289sylan2br 484 . . . . . . . . . . 11 coeff coeff
291 id 22 . . . . . . . . . . . . . 14
292291, 260syl6eqr 2523 . . . . . . . . . . . . 13
293292fveq2d 5883 . . . . . . . . . . . 12 coeff coeff
294292oveq2d 6324 . . . . . . . . . . . . 13
295294fveq2d 5883 . . . . . . . . . . . 12 coeff coeff
296293, 295oveq12d 6326 . . . . . . . . . . 11 coeff coeff coeff coeff
297266, 290, 296fsump1 13894 . . . . . . . . . 10 coeff coeff coeff coeff coeff coeff
298262, 297syl5eq 2517 . . . . . . . . 9 coeff coeff coeff coeff coeff coeff
299 eldifn 3545 . . . . . . . . . . . . . 14
300299adantl 473 . . . . . . . . . . . . 13
301 eldifi 3544 . . . . . . . . . . . . . . . . 17
302 elfznn0 11913 . . . . . . . . . . . . . . . . 17
303301, 302syl 17 . . . . . . . . . . . . . . . 16
304176, 169dgrub 23267 . . . . . . . . . . . . . . . . 17 Poly coeff deg
3053043expia 1233 . . . . . . . . . . . . . . . 16 Poly coeff deg
30669, 303, 305syl2an 485 . . . . . . . . . . . . . . 15 coeff deg
307 elfzuz 11822 . . . . . . . . . . . . . . . . . . 19
308301, 307syl 17 . . . . . . . . . . . . . . . . . 18
309308adantl 473 . . . . . . . . . . . . . . . . 17
310 1z 10991 . . . . . . . . . . . . . . . . 17
311 elfz5 11818 . . . . . . . . . . . . . . . . 17
312309, 310, 311sylancl 675 . . . . . . . . . . . . . . . 16
313161breq2d 4407 . . . . . . . . . . . . . . . . 17 deg
314313adantr 472 . . . . . . . . . . . . . . . 16 deg
315312, 314bitr4d 264 . . . . . . . . . . . . . . 15 deg
316306, 315sylibrd 242 . . . . . . . . . . . . . 14 coeff
317316necon1bd 2661 . . . . . . . . . . . . 13 coeff
318300, 317mpd 15 . . . . . . . . . . . 12 coeff
319318oveq1d 6323 . . . . . . . . . . 11 coeff coeff coeff
320301, 287sylan2 482 . . . . . . . . . . . 12 coeff
321320mul02d 9849 . . . . . . . . . . 11 coeff
322319, 321eqtrd 2505 . . . . . . . . . 10 coeff coeff
323 fzfid 12224 . . . . . . . . . 10
324283, 289, 322, 323fsumss 13868 . . . . . . . . 9 coeff coeff coeff coeff
325 0z 10972 . . . . . . . . . . . 12
326189fveq1d 5881 . . . . . . . . . . . . . . 15 coeff coeff coeff
327 coeidp 23296 . . . . . . . . . . . . . . . . . . . 20 coeff
328162nesymi 2700 . . . . . . . . . . . . . . . . . . . . 21
329328iffalsei 3882 . . . . . . . . . . . . . . . . . . . 20
330327, 329syl6eq 2521 . . . . . . . . . . . . . . . . . . 19 coeff
331330adantl 473 . . . . . . . . . . . . . . . . . 18 coeff
332 0cn 9653 . . . . . . . . . . . . . . . . . . . . 21
333 vex 3034 . . . . . . . . . . . . . . . . . . . . . 22
334333fvconst2 6136 . . . . . . . . . . . . . . . . . . . . 21
335332, 334ax-mp 5 . . . . . . . . . . . . . . . . . . . 20
336187coefv0 23281 . . . . . . . . . . . . . . . . . . . . 21 Poly coeff
337185, 336syl 17 . . . . . . . . . . . . . . . . . . . 20 coeff
338335, 337syl5reqr 2520 . . . . . . . . . . . . . . . . . . 19 coeff
339338adantr 472 . . . . . . . . . . . . . . . . . 18 coeff
340195, 198, 200, 200, 201, 331, 339ofval 6559 . . . . . . . . . . . . . . . . 17 coeff coeff
341263, 340mpan2 685 . . . . . . . . . . . . . . . 16 coeff coeff
342 df-neg 9883 . . . . . . . . . . . . . . . 16
343341, 342syl6eqr 2523 . . . . . . . . . . . . . . 15 coeff coeff
344326, 343eqtrd 2505 . . . . . . . . . . . . . 14 coeff
345277oveq1d 6323 . . . . . . . . . . . . . . . . 17
346103subid1d 9994 . . . . . . . . . . . . . . . . 17
347345, 346, 313eqtrd 2509 . . . . . . . . . . . . . . . 16 deg
348347fveq2d 5883 . . . . . . . . . . . . . . 15 coeff coeffdeg
349348, 235eqtr4d 2508 . . . . . . . . . . . . . 14 coeff
350344, 349oveq12d 6326 . . . . . . . . . . . . 13 coeff coeff
351350, 252eqeltrd 2549 . . . . . . . . . . . 12 coeff coeff
352 fveq2 5879 . . . . . . . . . . . . . 14 coeff coeff
353 oveq2 6316 . . . . . . . . . . . . . . 15
354353fveq2d 5883 . . . . . . . . . . . . . 14 coeff coeff
355352, 354oveq12d 6326 . . . . . . . . . . . . 13 coeff coeff coeff coeff
356355fsum1 13885 . . . . . . . . . . . 12 coeff coeff coeff coeff coeff coeff
357325, 351, 356sylancr 676 . . . . . . . . . . 11 coeff coeff coeff coeff
358357, 350eqtrd 2505 . . . . . . . . . 10 coeff coeff
359277oveq1d 6323 . . . . . . . . . . . . 13
360359fveq2d 5883 . . . . . . . . . . . 12 coeff coeff
361227, 360oveq12d 6326 . . . . . . . . . . 11 coeff coeff coeff
362244mulid2d 9679 . . . . . . . . . . 11 coeff coeff
363361, 362eqtrd 2505 . . . . . . . . . 10 coeff coeff coeff
364358, 363oveq12d 6326 . . . . . . . . 9 coeff coeff coeff coeff coeff
365298, 324, 3643eqtr3rd 2514 . . . . . . . 8 coeff coeff coeff
366258, 259, 3653eqtr4rd 2516 . . . . . . 7 coeff
367366oveq1d 6323 . . . . . 6 coeff
368240, 245, 249divcan4d 10411 . . . . . . 7
369368oveq1d 6323 . . . . . 6 coeff coeff
370253, 367, 3693eqtr3rd 2514 . . . . 5 coeff
371370negeqd 9889 . . . 4 coeff
372251, 371eqtr3d 2507 . . 3 coeff
373129, 239, 3723eqtrd 2509 . 2
37425, 373exlimddv 1789 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 189   wo 375   wa 376   w3a 1007   wceq 1452  wex 1671   wcel 1904   wne 2641  wral 2756  cvv 3031   cdif 3387   cun 3388   cin 3389   wss 3390  c0 3722  cif 3872  csn 3959   class class class wbr 4395   cxp 4837  ccnv 4838   cdm 4839  cima 4842   wfn 5584  wf 5585  cfv 5589  (class class class)co 6308   cof 6548  cfn 7587  cc 9555  cr 9556  cc0 9557  c1 9558   caddc 9560   cmul 9562   clt 9693   cle 9694   cmin 9880  cneg 9881   cdiv 10291  cn 10631  cn0 10893  cz 10961  cuz 11182  cfz 11810  chash 12553  csu 13829  c0p 22706  Polycply 23217  cidp 23218  coeffccoe 23219  degcdgr 23220   quot cquot 23322 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-inf2 8164  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634  ax-pre-sup 9635  ax-addf 9636 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-fal 1458  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-se 4799  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-isom 5598  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-of 6550  df-om 6712  df-1st 6812  df-2nd 6813  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-oadd 7204  df-er 7381  df-map 7492  df-pm 7493  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-sup 7974  df-inf 7975  df-oi 8043  df-card 8391  df-cda 8616  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-div 10292  df-nn 10632  df-2 10690  df-3 10691  df-n0 10894  df-z 10962  df-uz 11183  df-rp 11326  df-fz 11811  df-fzo 11943  df-fl 12061  df-seq 12252  df-exp 12311  df-hash 12554  df-cj 13239  df-re 13240  df-im 13241  df-sqrt 13375  df-abs 13376  df-clim 13629  df-rlim 13630  df-sum 13830  df-0p 22707  df-ply 23221  df-idp 23222  df-coe 23223  df-dgr 23224  df-quot 23323 This theorem is referenced by:  vieta1  23344
 Copyright terms: Public domain W3C validator