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

Theorem vieta1lem2 20181
 Description: Lemma for vieta1 20182: 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 9973 . . . . . . 7
52, 4eqeltrrd 2479 . . . . . 6
65nnne0d 10000 . . . . 5
71, 6eqnetrd 2585 . . . 4
8 vieta1.4 . . . . . . . 8 Poly
9 vieta1.2 . . . . . . . . . 10 deg
109, 6syl5eqner 2592 . . . . . . . . 9 deg
11 fveq2 5687 . . . . . . . . . . 11 deg deg
12 dgr0 20133 . . . . . . . . . . 11 deg
1311, 12syl6eq 2452 . . . . . . . . . 10 deg
1413necon3i 2606 . . . . . . . . 9 deg
1510, 14syl 16 . . . . . . . 8
16 vieta1.3 . . . . . . . . 9
1716fta1 20178 . . . . . . . 8 Poly deg
188, 15, 17syl2anc 643 . . . . . . 7 deg
1918simpld 446 . . . . . 6
20 hasheq0 11599 . . . . . 6
2119, 20syl 16 . . . . 5
2221necon3bid 2602 . . . 4
237, 22mpbid 202 . . 3
24 n0 3597 . . 3
2523, 24sylib 189 . 2
26 incom 3493 . . . . 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 20180 . . . . . . . . . 10 Poly deg
3130simprd 450 . . . . . . . . 9 deg
3230simpld 446 . . . . . . . . . . 11 Poly
33 dgrcl 20105 . . . . . . . . . . 11 Poly deg
3432, 33syl 16 . . . . . . . . . 10 deg
3534nn0red 10231 . . . . . . . . 9 deg
3631, 35eqeltrd 2478 . . . . . . . 8
3736ltp1d 9897 . . . . . . . 8
3836, 37gtned 9164 . . . . . . 7
39 snssi 3902 . . . . . . . . . . 11
40 ssequn1 3477 . . . . . . . . . . 11
4139, 40sylib 189 . . . . . . . . . 10
4241fveq2d 5691 . . . . . . . . 9
438adantr 452 . . . . . . . . . . . . . . . . . 18 Poly
44 cnvimass 5183 . . . . . . . . . . . . . . . . . . . . 21
4516, 44eqsstri 3338 . . . . . . . . . . . . . . . . . . . 20
46 plyf 20070 . . . . . . . . . . . . . . . . . . . . 21 Poly
47 fdm 5554 . . . . . . . . . . . . . . . . . . . . 21
488, 46, 473syl 19 . . . . . . . . . . . . . . . . . . . 20
4945, 48syl5sseq 3356 . . . . . . . . . . . . . . . . . . 19
5049sselda 3308 . . . . . . . . . . . . . . . . . 18
5116eleq2i 2468 . . . . . . . . . . . . . . . . . . . 20
528, 46syl 16 . . . . . . . . . . . . . . . . . . . . 21
53 ffn 5550 . . . . . . . . . . . . . . . . . . . . 21
54 fniniseg 5810 . . . . . . . . . . . . . . . . . . . . 21
5552, 53, 543syl 19 . . . . . . . . . . . . . . . . . . . 20
5651, 55syl5bb 249 . . . . . . . . . . . . . . . . . . 19
5756simplbda 608 . . . . . . . . . . . . . . . . . 18
58 eqid 2404 . . . . . . . . . . . . . . . . . . 19
5958facth 20176 . . . . . . . . . . . . . . . . . 18 Poly quot
6043, 50, 57, 59syl3anc 1184 . . . . . . . . . . . . . . . . 17 quot
6129oveq2i 6051 . . . . . . . . . . . . . . . . 17 quot
6260, 61syl6eqr 2454 . . . . . . . . . . . . . . . 16
6362cnveqd 5007 . . . . . . . . . . . . . . 15
6463imaeq1d 5161 . . . . . . . . . . . . . 14
6516, 64syl5eq 2448 . . . . . . . . . . . . 13
66 cnex 9027 . . . . . . . . . . . . . . 15
6766a1i 11 . . . . . . . . . . . . . 14
6858plyremlem 20174 . . . . . . . . . . . . . . . . 17 Poly deg
6950, 68syl 16 . . . . . . . . . . . . . . . 16 Poly deg
7069simp1d 969 . . . . . . . . . . . . . . 15 Poly
71 plyf 20070 . . . . . . . . . . . . . . 15 Poly
7270, 71syl 16 . . . . . . . . . . . . . 14
73 plyf 20070 . . . . . . . . . . . . . . 15 Poly
7432, 73syl 16 . . . . . . . . . . . . . 14
75 ofmulrt 20152 . . . . . . . . . . . . . 14
7667, 72, 74, 75syl3anc 1184 . . . . . . . . . . . . 13
7769simp3d 971 . . . . . . . . . . . . . 14
7877uneq1d 3460 . . . . . . . . . . . . 13
7965, 76, 783eqtrd 2440 . . . . . . . . . . . 12
8079fveq2d 5691 . . . . . . . . . . 11
811, 2eqtr4d 2439 . . . . . . . . . . . 12
8281adantr 452 . . . . . . . . . . 11
8380, 82eqtr3d 2438 . . . . . . . . . 10
8415adantr 452 . . . . . . . . . . . . . . . . . 18
8562, 84eqnetrrd 2587 . . . . . . . . . . . . . . . . 17
86 plymul0or 20151 . . . . . . . . . . . . . . . . . . 19 Poly Poly
8770, 32, 86syl2anc 643 . . . . . . . . . . . . . . . . . 18
8887necon3abid 2600 . . . . . . . . . . . . . . . . 17
8985, 88mpbid 202 . . . . . . . . . . . . . . . 16
90 neanior 2652 . . . . . . . . . . . . . . . 16
9189, 90sylibr 204 . . . . . . . . . . . . . . 15
9291simprd 450 . . . . . . . . . . . . . 14
93 eqid 2404 . . . . . . . . . . . . . . 15
9493fta1 20178 . . . . . . . . . . . . . 14 Poly deg
9532, 92, 94syl2anc 643 . . . . . . . . . . . . 13 deg
9695simprd 450 . . . . . . . . . . . 12 deg
9796, 31breqtrrd 4198 . . . . . . . . . . 11
98 snfi 7146 . . . . . . . . . . . . . 14
9995simpld 446 . . . . . . . . . . . . . 14
100 hashun2 11612 . . . . . . . . . . . . . 14
10198, 99, 100sylancr 645 . . . . . . . . . . . . 13
102 ax-1cn 9004 . . . . . . . . . . . . . . 15
1033nncnd 9972 . . . . . . . . . . . . . . . 16
104103adantr 452 . . . . . . . . . . . . . . 15
105 addcom 9208 . . . . . . . . . . . . . . 15
106102, 104, 105sylancr 645 . . . . . . . . . . . . . 14
10783, 106eqtr4d 2439 . . . . . . . . . . . . 13
108 hashsng 11602 . . . . . . . . . . . . . . 15
109108adantl 453 . . . . . . . . . . . . . 14
110109oveq1d 6055 . . . . . . . . . . . . 13
111101, 107, 1103brtr3d 4201 . . . . . . . . . . . 12
112 hashcl 11594 . . . . . . . . . . . . . . 15
11399, 112syl 16 . . . . . . . . . . . . . 14
114113nn0red 10231 . . . . . . . . . . . . 13
115 1re 9046 . . . . . . . . . . . . . 14
116115a1i 11 . . . . . . . . . . . . 13
11736, 114, 116leadd2d 9577 . . . . . . . . . . . 12
118111, 117mpbird 224 . . . . . . . . . . 11
119114, 36letri3d 9171 . . . . . . . . . . 11
12097, 118, 119mpbir2and 889 . . . . . . . . . 10
12183, 120eqeq12d 2418 . . . . . . . . 9
12242, 121syl5ib 211 . . . . . . . 8
123122necon3ad 2603 . . . . . . 7
12438, 123mpd 15 . . . . . 6
125 disjsn 3828 . . . . . 6
126124, 125sylibr 204 . . . . 5
12726, 126syl5eq 2448 . . . 4
12819adantr 452 . . . 4
12949adantr 452 . . . . 5
130129sselda 3308 . . . 4
131127, 79, 128, 130fsumsplit 12488 . . 3
132 id 20 . . . . . . 7
133132sumsn 12489 . . . . . 6
13450, 50, 133syl2anc 643 . . . . 5
13550negnegd 9358 . . . . 5
136134, 135eqtr4d 2439 . . . 4
137120, 31eqtrd 2436 . . . . . 6 deg
13828adantr 452 . . . . . . 7 Poly deg deg coeffdeg coeffdeg
139 fveq2 5687 . . . . . . . . . . 11 deg deg
140139eqeq2d 2415 . . . . . . . . . 10 deg deg
141 cnveq 5005 . . . . . . . . . . . . 13
142141imaeq1d 5161 . . . . . . . . . . . 12
143142fveq2d 5691 . . . . . . . . . . 11
144143, 139eqeq12d 2418 . . . . . . . . . 10 deg deg
145140, 144anbi12d 692 . . . . . . . . 9 deg deg deg deg
146142sumeq1d 12450 . . . . . . . . . 10
147 fveq2 5687 . . . . . . . . . . . . 13 coeff coeff
148139oveq1d 6055 . . . . . . . . . . . . 13 deg deg
149147, 148fveq12d 5693 . . . . . . . . . . . 12 coeffdeg coeffdeg
150147, 139fveq12d 5693 . . . . . . . . . . . 12 coeffdeg coeffdeg
151149, 150oveq12d 6058 . . . . . . . . . . 11 coeffdeg coeffdeg coeffdeg coeffdeg
152151negeqd 9256 . . . . . . . . . 10 coeffdeg coeffdeg coeffdeg coeffdeg
153146, 152eqeq12d 2418 . . . . . . . . 9 coeffdeg coeffdeg coeffdeg coeffdeg
154145, 153imbi12d 312 . . . . . . . 8 deg deg coeffdeg coeffdeg deg deg coeffdeg coeffdeg
155154rspcv 3008 . . . . . . 7 Poly Poly deg deg coeffdeg coeffdeg deg deg coeffdeg coeffdeg
15632, 138, 155sylc 58 . . . . . 6 deg deg coeffdeg coeffdeg
15731, 137, 156mp2and 661 . . . . 5 coeffdeg coeffdeg
15831oveq1d 6055 . . . . . . . 8 deg
159158fveq2d 5691 . . . . . . 7 coeff coeffdeg
16062fveq2d 5691 . . . . . . . . . 10 coeff coeff
16127, 160syl5eq 2448 . . . . . . . . 9 coeff
16262fveq2d 5691 . . . . . . . . . . 11 deg deg
16369simp2d 970 . . . . . . . . . . . . . 14 deg
164 ax-1ne0 9015 . . . . . . . . . . . . . . 15
165164a1i 11 . . . . . . . . . . . . . 14
166163, 165eqnetrd 2585 . . . . . . . . . . . . 13 deg
167 fveq2 5687 . . . . . . . . . . . . . . 15 deg deg
168167, 12syl6eq 2452 . . . . . . . . . . . . . 14 deg
169168necon3i 2606 . . . . . . . . . . . . 13 deg
170166, 169syl 16 . . . . . . . . . . . 12
171 eqid 2404 . . . . . . . . . . . . 13 deg deg
172 eqid 2404 . . . . . . . . . . . . 13 deg deg
173171, 172dgrmul 20141 . . . . . . . . . . . 12 Poly Poly deg deg deg
17470, 170, 32, 92, 173syl22anc 1185 . . . . . . . . . . 11 deg deg deg
175162, 174eqtrd 2436 . . . . . . . . . 10 deg deg deg
1769, 175syl5eq 2448 . . . . . . . . 9 deg deg
177161, 176fveq12d 5693 . . . . . . . 8 coeff deg deg
178 eqid 2404 . . . . . . . . . 10 coeff coeff
179 eqid 2404 . . . . . . . . . 10 coeff coeff
180178, 179, 171, 172coemulhi 20125 . . . . . . . . 9 Poly Poly coeff deg deg coeff deg coeffdeg
18170, 32, 180syl2anc 643 . . . . . . . 8 coeff deg deg coeff deg coeffdeg
182163fveq2d 5691 . . . . . . . . . . 11 coeff deg coeff
183 ssid 3327 . . . . . . . . . . . . . . 15
184 plyid 20081 . . . . . . . . . . . . . . 15 Poly
185183, 102, 184mp2an 654 . . . . . . . . . . . . . 14 Poly
186 plyconst 20078 . . . . . . . . . . . . . . 15 Poly
187183, 50, 186sylancr 645 . . . . . . . . . . . . . 14 Poly
188 eqid 2404 . . . . . . . . . . . . . . 15 coeff coeff
189 eqid 2404 . . . . . . . . . . . . . . 15 coeff coeff
190188, 189coesub 20128 . . . . . . . . . . . . . 14 Poly Poly coeff coeff coeff
191185, 187, 190sylancr 645 . . . . . . . . . . . . 13 coeff coeff coeff
192191fveq1d 5689 . . . . . . . . . . . 12 coeff coeff coeff
193 1nn0 10193 . . . . . . . . . . . . . 14
194188coef3 20104 . . . . . . . . . . . . . . . . 17 Poly coeff
195 ffn 5550 . . . . . . . . . . . . . . . . 17 coeff coeff
196185, 194, 195mp2b 10 . . . . . . . . . . . . . . . 16 coeff
197196a1i 11 . . . . . . . . . . . . . . 15 coeff
198189coef3 20104 . . . . . . . . . . . . . . . 16 Poly coeff
199 ffn 5550 . . . . . . . . . . . . . . . 16 coeff coeff
200187, 198, 1993syl 19 . . . . . . . . . . . . . . 15 coeff
201 nn0ex 10183 . . . . . . . . . . . . . . . 16
202201a1i 11 . . . . . . . . . . . . . . 15
203 inidm 3510 . . . . . . . . . . . . . . 15
204 coeidp 20134 . . . . . . . . . . . . . . . . 17 coeff
205204adantl 453 . . . . . . . . . . . . . . . 16 coeff
206 eqid 2404 . . . . . . . . . . . . . . . . 17
207 iftrue 3705 . . . . . . . . . . . . . . . . 17
208206, 207ax-mp 8 . . . . . . . . . . . . . . . 16
209205, 208syl6eq 2452 . . . . . . . . . . . . . . 15 coeff
210 0lt1 9506 . . . . . . . . . . . . . . . . . 18
211 0re 9047 . . . . . . . . . . . . . . . . . . 19
212211, 115ltnlei 9150 . . . . . . . . . . . . . . . . . 18
213210, 212mpbi 200 . . . . . . . . . . . . . . . . 17
21450adantr 452 . . . . . . . . . . . . . . . . . . 19
215 0dgr 20117 . . . . . . . . . . . . . . . . . . 19 deg
216214, 215syl 16 . . . . . . . . . . . . . . . . . 18 deg
217216breq2d 4184 . . . . . . . . . . . . . . . . 17 deg
218213, 217mtbiri 295 . . . . . . . . . . . . . . . 16 deg
219 eqid 2404 . . . . . . . . . . . . . . . . . . . 20 deg deg
220189, 219dgrub 20106 . . . . . . . . . . . . . . . . . . 19 Poly coeff deg
2212203expia 1155 . . . . . . . . . . . . . . . . . 18 Poly coeff deg
222187, 221sylan 458 . . . . . . . . . . . . . . . . 17 coeff deg
223222necon1bd 2635 . . . . . . . . . . . . . . . 16 deg coeff
224218, 223mpd 15 . . . . . . . . . . . . . . 15 coeff
225197, 200, 202, 202, 203, 209, 224ofval 6273 . . . . . . . . . . . . . 14 coeff coeff
226193, 225mpan2 653 . . . . . . . . . . . . 13 coeff coeff
227102subid1i 9328 . . . . . . . . . . . . 13
228226, 227syl6eq 2452 . . . . . . . . . . . 12 coeff coeff
229192, 228eqtrd 2436 . . . . . . . . . . 11 coeff
230182, 229eqtrd 2436 . . . . . . . . . 10 coeff deg
231230oveq1d 6055 . . . . . . . . 9 coeff deg coeffdeg coeffdeg
232179coef3 20104 . . . . . . . . . . . 12 Poly coeff
23332, 232syl 16 . . . . . . . . . . 11 coeff
234233, 34ffvelrnd 5830 . . . . . . . . . 10 coeffdeg
235234mulid2d 9062 . . . . . . . . 9 coeffdeg coeffdeg
236231, 235eqtrd 2436 . . . . . . . 8 coeff deg coeffdeg coeffdeg
237177, 181, 2363eqtrd 2440 . . . . . . 7 coeffdeg
238159, 237oveq12d 6058 . . . . . 6 coeff coeffdeg coeffdeg
239238negeqd 9256 . . . . 5 coeff coeffdeg coeffdeg
240157, 239eqtr4d 2439 . . . 4 coeff
241136, 240oveq12d 6058 . . 3 coeff
24250negcld 9354 . . . . 5
243 nnm1nn0 10217 . . . . . . . . 9
2443, 243syl 16 . . . . . . . 8
245244adantr 452 . . . . . . 7
246233, 245ffvelrnd 5830 . . . . . 6 coeff
247237, 234eqeltrd 2478 . . . . . 6
2489, 27dgreq0 20136 . . . . . . . . 9 Poly
24943, 248syl 16 . . . . . . . 8
250249necon3bid 2602 . . . . . . 7
25184, 250mpbid 202 . . . . . 6
252246, 247, 251divcld 9746 . . . . 5 coeff
253242, 252negdid 9380 . . . 4 coeff coeff
254242, 247mulcld 9064 . . . . . . 7
255254, 246, 247, 251divdird 9784 . . . . . 6 coeff coeff
256 nnm1nn0 10217 . . . . . . . . . . 11
2575, 256syl 16 . . . . . . . . . 10
258257adantr 452 . . . . . . . . 9
259178, 179coemul 20123 . . . . . . . . 9 Poly Poly coeff coeff coeff
26070, 32, 258, 259syl3anc 1184 . . . . . . . 8 coeff coeff coeff
261161fveq1d 5689 . . . . . . . 8 coeff
262 1e0p1 10366 . . . . . . . . . . . 12
263262oveq2i 6051 . . . . . . . . . . 11
264263sumeq1i 12447 . . . . . . . . . 10 coeff coeff coeff coeff
265 0nn0 10192 . . . . . . . . . . . . 13
266 nn0uz 10476 . . . . . . . . . . . . 13
267265, 266eleqtri 2476 . . . . . . . . . . . 12
268267a1i 11 . . . . . . . . . . 11
269263eleq2i 2468 . . . . . . . . . . . 12
270178coef3 20104 . . . . . . . . . . . . . . 15 Poly coeff
27170, 270syl 16 . . . . . . . . . . . . . 14 coeff
272 elfznn0 11039 . . . . . . . . . . . . . 14
273 ffvelrn 5827 . . . . . . . . . . . . . 14 coeff coeff
274271, 272, 273syl2an 464 . . . . . . . . . . . . 13 coeff
2752oveq1d 6055 . . . . . . . . . . . . . . . . . . . 20
276 pncan 9267 . . . . . . . . . . . . . . . . . . . . 21
277103, 102, 276sylancl 644 . . . . . . . . . . . . . . . . . . . 20
278275, 277eqtr3d 2438 . . . . . . . . . . . . . . . . . . 19
279278adantr 452 . . . . . . . . . . . . . . . . . 18
2803adantr 452 . . . . . . . . . . . . . . . . . 18
281279, 280eqeltrd 2478 . . . . . . . . . . . . . . . . 17
282 nnuz 10477 . . . . . . . . . . . . . . . . 17
283281, 282syl6eleq 2494 . . . . . . . . . . . . . . . 16
284 fzss2 11048 . . . . . . . . . . . . . . . 16
285283, 284syl 16 . . . . . . . . . . . . . . 15
286285sselda 3308 . . . . . . . . . . . . . 14
287 fznn0sub 11041 . . . . . . . . . . . . . . 15
288 ffvelrn 5827 . . . . . . . . . . . . . . 15 coeff coeff
289233, 287, 288syl2an 464 . . . . . . . . . . . . . 14 coeff
290286, 289syldan 457 . . . . . . . . . . . . 13 coeff
291274, 290mulcld 9064 . . . . . . . . . . . 12 coeff coeff
292269, 291sylan2br 463 . . . . . . . . . . 11 coeff coeff
293 id 20 . . . . . . . . . . . . . 14
294293, 262syl6eqr 2454 . . . . . . . . . . . . 13
295294fveq2d 5691 . . . . . . . . . . . 12 coeff coeff
296294oveq2d 6056 . . . . . . . . . . . . 13
297296fveq2d 5691 . . . . . . . . . . . 12 coeff coeff
298295, 297oveq12d 6058 . . . . . . . . . . 11 coeff coeff coeff coeff
299268, 292, 298fsump1 12495 . . . . . . . . . 10 coeff coeff coeff coeff coeff coeff
300264, 299syl5eq 2448 . . . . . . . . 9 coeff coeff coeff coeff coeff coeff
301 eldifn 3430 . . . . . . . . . . . . . 14
302301adantl 453 . . . . . . . . . . . . 13
303 eldifi 3429 . . . . . . . . . . . . . . . . 17
304 elfznn0 11039 . . . . . . . . . . . . . . . . 17
305303, 304syl 16 . . . . . . . . . . . . . . . 16
306178, 171dgrub 20106 . . . . . . . . . . . . . . . . 17 Poly coeff deg
3073063expia 1155 . . . . . . . . . . . . . . . 16 Poly coeff deg
30870, 305, 307syl2an 464 . . . . . . . . . . . . . . 15 coeff deg
309 elfzuz 11011 . . . . . . . . . . . . . . . . . . 19
310303, 309syl 16 . . . . . . . . . . . . . . . . . 18
311310adantl 453 . . . . . . . . . . . . . . . . 17
312 1z 10267 . . . . . . . . . . . . . . . . 17
313 elfz5 11007 . . . . . . . . . . . . . . . . 17
314311, 312, 313sylancl 644 . . . . . . . . . . . . . . . 16
315163breq2d 4184 . . . . . . . . . . . . . . . . 17 deg
316315adantr 452 . . . . . . . . . . . . . . . 16 deg
317314, 316bitr4d 248 . . . . . . . . . . . . . . 15 deg
318308, 317sylibrd 226 . . . . . . . . . . . . . 14 coeff
319318necon1bd 2635 . . . . . . . . . . . . 13 coeff
320302, 319mpd 15 . . . . . . . . . . . 12 coeff
321320oveq1d 6055 . . . . . . . . . . 11 coeff coeff coeff
322303, 289sylan2 461 . . . . . . . . . . . 12 coeff
323322mul02d 9220 . . . . . . . . . . 11 coeff
324321, 323eqtrd 2436 . . . . . . . . . 10 coeff coeff
325 fzfid 11267 . . . . . . . . . 10
326285, 291, 324, 325fsumss 12474 . . . . . . . . 9 coeff coeff coeff coeff
327 0z 10249 . . . . . . . . . . . 12
328191fveq1d 5689 . . . . . . . . . . . . . . 15 coeff coeff coeff
329 coeidp 20134 . . . . . . . . . . . . . . . . . . . 20 coeff
330164necomi 2649 . . . . . . . . . . . . . . . . . . . . . 22
331 df-ne 2569 . . . . . . . . . . . . . . . . . . . . . 22
332330, 331mpbi 200 . . . . . . . . . . . . . . . . . . . . 21
333 iffalse 3706 . . . . . . . . . . . . . . . . . . . . 21
334332, 333ax-mp 8 . . . . . . . . . . . . . . . . . . . 20
335329, 334syl6eq 2452 . . . . . . . . . . . . . . . . . . 19 coeff
336335adantl 453 . . . . . . . . . . . . . . . . . 18 coeff
337 0cn 9040 . . . . . . . . . . . . . . . . . . . . 21
338 vex 2919 . . . . . . . . . . . . . . . . . . . . . 22
339338fvconst2 5906 . . . . . . . . . . . . . . . . . . . . 21
340337, 339ax-mp 8 . . . . . . . . . . . . . . . . . . . 20
341189coefv0 20119 . . . . . . . . . . . . . . . . . . . . 21 Poly coeff
342187, 341syl 16 . . . . . . . . . . . . . . . . . . . 20 coeff
343340, 342syl5reqr 2451 . . . . . . . . . . . . . . . . . . 19 coeff
344343adantr 452 . . . . . . . . . . . . . . . . . 18 coeff
345197, 200, 202, 202, 203, 336, 344ofval 6273 . . . . . . . . . . . . . . . . 17 coeff coeff
346265, 345mpan2 653 . . . . . . . . . . . . . . . 16 coeff coeff
347 df-neg 9250 . . . . . . . . . . . . . . . 16
348346, 347syl6eqr 2454 . . . . . . . . . . . . . . 15 coeff coeff
349328, 348eqtrd 2436 . . . . . . . . . . . . . 14 coeff
350279oveq1d 6055 . . . . . . . . . . . . . . . . 17
351104subid1d 9356 . . . . . . . . . . . . . . . . 17
352350, 351, 313eqtrd 2440 . . . . . . . . . . . . . . . 16 deg
353352fveq2d 5691 . . . . . . . . . . . . . . 15 coeff coeffdeg
354353, 237eqtr4d 2439 . . . . . . . . . . . . . 14 coeff
355349, 354oveq12d 6058 . . . . . . . . . . . . 13 coeff coeff
356355, 254eqeltrd 2478 . . . . . . . . . . . 12 coeff coeff
357 fveq2 5687 . . . . . . . . . . . . . 14 coeff coeff
358 oveq2 6048 . . . . . . . . . . . . . . 15
359358fveq2d 5691 . . . . . . . . . . . . . 14 coeff coeff
360357, 359oveq12d 6058 . . . . . . . . . . . . 13 coeff coeff coeff coeff
361360fsum1 12490 . . . . . . . . . . . 12 coeff coeff coeff coeff coeff coeff
362327, 356, 361sylancr 645 . . . . . . . . . . 11 coeff coeff coeff coeff
363362, 355eqtrd 2436 . . . . . . . . . 10 coeff coeff
364279oveq1d 6055 . . . . . . . . . . . . 13
365364fveq2d 5691 . . . . . . . . . . . 12 coeff coeff
366229, 365oveq12d 6058 . . . . . . . . . . 11 coeff coeff coeff
367246mulid2d 9062 . . . . . . . . . . 11 coeff coeff
368366, 367eqtrd 2436 . . . . . . . . . 10 coeff coeff coeff
369363, 368oveq12d 6058 . . . . . . . . 9 coeff coeff coeff coeff coeff
370300, 326, 3693eqtr3rd 2445 . . . . . . . 8 coeff coeff coeff
371260, 261, 3703eqtr4rd 2447 . . . . . . 7 coeff
372371oveq1d 6055 . . . . . 6 coeff
373242, 247, 251divcan4d 9752 . . . . . . 7
374373oveq1d 6055 . . . . . 6 coeff coeff
375255, 372, 3743eqtr3rd 2445 . . . . 5 coeff
376375negeqd 9256 . . . 4 coeff
377253, 376eqtr3d 2438 . . 3 coeff
378131, 241, 3773eqtrd 2440 . 2
37925, 378exlimddv 1645 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wo 358   wa 359   w3a 936  wex 1547   wceq 1649   wcel 1721   wne 2567  wral 2666  cvv 2916   cdif 3277   cun 3278   cin 3279   wss 3280  c0 3588  cif 3699  csn 3774   class class class wbr 4172   cxp 4835  ccnv 4836   cdm 4837  cima 4840   wfn 5408  wf 5409  cfv 5413  (class class class)co 6040   cof 6262  cfn 7068  cc 8944  cr 8945  cc0 8946  c1 8947   caddc 8949   cmul 8951   clt 9076   cle 9077   cmin 9247  cneg 9248   cdiv 9633  cn 9956  cn0 10177  cz 10238  cuz 10444  cfz 10999  chash 11573  csu 12434  c0p 19514  Polycply 20056  cidp 20057  coeffccoe 20058  degcdgr 20059   quot cquot 20160 This theorem is referenced by:  vieta1  20182 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-inf2 7552  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-pre-sup 9024  ax-addf 9025 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-of 6264  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-oadd 6687  df-er 6864  df-map 6979  df-pm 6980  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-sup 7404  df-oi 7435  df-card 7782  df-cda 8004  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-n0 10178  df-z 10239  df-uz 10445  df-rp 10569  df-fz 11000  df-fzo 11091  df-fl 11157  df-seq 11279  df-exp 11338  df-hash 11574  df-cj 11859  df-re 11860  df-im 11861  df-sqr 11995  df-abs 11996  df-clim 12237  df-rlim 12238  df-sum 12435  df-0p 19515  df-ply 20060  df-idp 20061  df-coe 20062  df-dgr 20063  df-quot 20161
 Copyright terms: Public domain W3C validator