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

Theorem aannenlem2 21911
 Description: Lemma for aannen 21913. (Contributed by Stefan O'Rear, 16-Nov-2014.)
Hypothesis
Ref Expression
aannenlem.a Poly deg coeff
Assertion
Ref Expression
aannenlem2
Distinct variable group:   ,,,,
Allowed substitution hints:   (,,,,)

Proof of Theorem aannenlem2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp3 990 . . . . . . . . . 10 Poly
2 eldifi 3576 . . . . . . . . . . . . . 14 Poly Poly
32adantr 465 . . . . . . . . . . . . 13 Poly Poly
433adant2 1007 . . . . . . . . . . . 12 Poly Poly
5 eldifsni 4099 . . . . . . . . . . . . . . 15 Poly
65adantr 465 . . . . . . . . . . . . . 14 Poly
7 0nn0 10695 . . . . . . . . . . . . . . . . . 18
8 dgrcl 21817 . . . . . . . . . . . . . . . . . . 19 Poly deg
93, 8syl 16 . . . . . . . . . . . . . . . . . 18 Poly deg
10 prssi 4127 . . . . . . . . . . . . . . . . . 18 deg deg
117, 9, 10sylancr 663 . . . . . . . . . . . . . . . . 17 Poly deg
12 ssrab2 3535 . . . . . . . . . . . . . . . . . 18 deg coeff
1312a1i 11 . . . . . . . . . . . . . . . . 17 Poly deg coeff
1411, 13unssd 3630 . . . . . . . . . . . . . . . 16 Poly deg deg coeff
15 nn0ssre 10684 . . . . . . . . . . . . . . . . 17
16 ressxr 9528 . . . . . . . . . . . . . . . . 17
1715, 16sstri 3463 . . . . . . . . . . . . . . . 16
1814, 17syl6ss 3466 . . . . . . . . . . . . . . 15 Poly deg deg coeff
19 fvex 5799 . . . . . . . . . . . . . . . . 17 deg
2019prid2 4082 . . . . . . . . . . . . . . . 16 deg deg
21 elun1 3621 . . . . . . . . . . . . . . . 16 deg deg deg deg deg coeff
2220, 21ax-mp 5 . . . . . . . . . . . . . . 15 deg deg deg coeff
23 supxrub 11388 . . . . . . . . . . . . . . 15 deg deg coeff deg deg deg coeff deg deg deg coeff
2418, 22, 23sylancl 662 . . . . . . . . . . . . . 14 Poly deg deg deg coeff
2518adantr 465 . . . . . . . . . . . . . . . 16 Poly deg deg coeff
26 fveq2 5789 . . . . . . . . . . . . . . . . . . . 20 coeff coeff
27 abs0 12876 . . . . . . . . . . . . . . . . . . . 20
2826, 27syl6eq 2508 . . . . . . . . . . . . . . . . . . 19 coeff coeff
29 c0ex 9481 . . . . . . . . . . . . . . . . . . . . 21
3029prid1 4081 . . . . . . . . . . . . . . . . . . . 20 deg
31 elun1 3621 . . . . . . . . . . . . . . . . . . . 20 deg deg deg coeff
3230, 31ax-mp 5 . . . . . . . . . . . . . . . . . . 19 deg deg coeff
3328, 32syl6eqel 2547 . . . . . . . . . . . . . . . . . 18 coeff coeff deg deg coeff
3433adantl 466 . . . . . . . . . . . . . . . . 17 Poly coeff coeff deg deg coeff
35 0z 10758 . . . . . . . . . . . . . . . . . . . . . . 23
36 eqid 2451 . . . . . . . . . . . . . . . . . . . . . . . 24 coeff coeff
3736coef2 21815 . . . . . . . . . . . . . . . . . . . . . . 23 Poly coeff
383, 35, 37sylancl 662 . . . . . . . . . . . . . . . . . . . . . 22 Poly coeff
3938ffvelrnda 5942 . . . . . . . . . . . . . . . . . . . . 21 Poly coeff
40 nn0abscl 12903 . . . . . . . . . . . . . . . . . . . . 21 coeff coeff
4139, 40syl 16 . . . . . . . . . . . . . . . . . . . 20 Poly coeff
4241adantr 465 . . . . . . . . . . . . . . . . . . 19 Poly coeff coeff
43 simplr 754 . . . . . . . . . . . . . . . . . . . . 21 Poly coeff
449ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 Poly coeff deg
453ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 Poly coeff Poly
46 simpr 461 . . . . . . . . . . . . . . . . . . . . . 22 Poly coeff coeff
47 eqid 2451 . . . . . . . . . . . . . . . . . . . . . . 23 deg deg
4836, 47dgrub 21818 . . . . . . . . . . . . . . . . . . . . . 22 Poly coeff deg
4945, 43, 46, 48syl3anc 1219 . . . . . . . . . . . . . . . . . . . . 21 Poly coeff deg
50 elfz2nn0 11581 . . . . . . . . . . . . . . . . . . . . 21 deg deg deg
5143, 44, 49, 50syl3anbrc 1172 . . . . . . . . . . . . . . . . . . . 20 Poly coeff deg
52 eqid 2451 . . . . . . . . . . . . . . . . . . . 20 coeff coeff
53 fveq2 5789 . . . . . . . . . . . . . . . . . . . . . . 23 coeff coeff
5453fveq2d 5793 . . . . . . . . . . . . . . . . . . . . . 22 coeff coeff
5554eqeq2d 2465 . . . . . . . . . . . . . . . . . . . . 21 coeff coeff coeff coeff
5655rspcev 3169 . . . . . . . . . . . . . . . . . . . 20 deg coeff coeff degcoeff coeff
5751, 52, 56sylancl 662 . . . . . . . . . . . . . . . . . . 19 Poly coeff degcoeff coeff
58 eqeq1 2455 . . . . . . . . . . . . . . . . . . . . 21 coeff coeff coeff coeff
5958rexbidv 2844 . . . . . . . . . . . . . . . . . . . 20 coeff deg coeff degcoeff coeff
6059elrab 3214 . . . . . . . . . . . . . . . . . . 19 coeff deg coeff coeff degcoeff coeff
6142, 57, 60sylanbrc 664 . . . . . . . . . . . . . . . . . 18 Poly coeff coeff deg coeff
62 elun2 3622 . . . . . . . . . . . . . . . . . 18 coeff deg coeff coeff deg deg coeff
6361, 62syl 16 . . . . . . . . . . . . . . . . 17 Poly coeff coeff deg deg coeff
6434, 63pm2.61dane 2766 . . . . . . . . . . . . . . . 16 Poly coeff deg deg coeff
65 supxrub 11388 . . . . . . . . . . . . . . . 16 deg deg coeff coeff deg deg coeff coeff deg deg coeff
6625, 64, 65syl2anc 661 . . . . . . . . . . . . . . 15 Poly coeff deg deg coeff
6766ralrimiva 2822 . . . . . . . . . . . . . 14 Poly coeff deg deg coeff
686, 24, 673jca 1168 . . . . . . . . . . . . 13 Poly deg deg deg coeff coeff deg deg coeff
69683adant2 1007 . . . . . . . . . . . 12 Poly deg deg deg coeff coeff deg deg coeff
70 neeq1 2729 . . . . . . . . . . . . . 14
71 fveq2 5789 . . . . . . . . . . . . . . 15 deg deg
7271breq1d 4400 . . . . . . . . . . . . . 14 deg deg deg coeff deg deg deg coeff
73 fveq2 5789 . . . . . . . . . . . . . . . . . 18 coeff coeff
7473fveq1d 5791 . . . . . . . . . . . . . . . . 17 coeff coeff
7574fveq2d 5793 . . . . . . . . . . . . . . . 16 coeff coeff
7675breq1d 4400 . . . . . . . . . . . . . . 15 coeff deg deg coeff coeff deg deg coeff
7776ralbidv 2839 . . . . . . . . . . . . . 14 coeff deg deg coeff coeff deg deg coeff
7870, 72, 773anbi123d 1290 . . . . . . . . . . . . 13 deg deg deg coeff coeff deg deg coeff deg deg deg coeff coeff deg deg coeff
7978elrab 3214 . . . . . . . . . . . 12 Poly deg deg deg coeff coeff deg deg coeff Poly deg deg deg coeff coeff deg deg coeff
804, 69, 79sylanbrc 664 . . . . . . . . . . 11 Poly Poly deg deg deg coeff coeff deg deg coeff
81 simp2 989 . . . . . . . . . . 11 Poly
82 fveq1 5788 . . . . . . . . . . . . 13
8382eqeq1d 2453 . . . . . . . . . . . 12
8483rspcev 3169 . . . . . . . . . . 11 Poly deg deg deg coeff coeff deg deg coeff Poly deg deg deg coeff coeff deg deg coeff
8580, 81, 84syl2anc 661 . . . . . . . . . 10 Poly Poly deg deg deg coeff coeff deg deg coeff
86 fveq2 5789 . . . . . . . . . . . . 13
8786eqeq1d 2453 . . . . . . . . . . . 12
8887rexbidv 2844 . . . . . . . . . . 11 Poly deg deg deg coeff coeff deg deg coeff Poly deg deg deg coeff coeff deg deg coeff
8988elrab 3214 . . . . . . . . . 10 Poly deg deg deg coeff coeff deg deg coeff Poly deg deg deg coeff coeff deg deg coeff
901, 85, 89sylanbrc 664 . . . . . . . . 9 Poly Poly deg deg deg coeff coeff deg deg coeff
91 prfi 7687 . . . . . . . . . . . . . . 15 deg
92 fzfi 11895 . . . . . . . . . . . . . . . . 17 deg
93 abrexfi 7712 . . . . . . . . . . . . . . . . 17 deg deg coeff
9492, 93ax-mp 5 . . . . . . . . . . . . . . . 16 deg coeff
95 rabssab 3537 . . . . . . . . . . . . . . . 16 deg coeff deg coeff
96 ssfi 7634 . . . . . . . . . . . . . . . 16 deg coeff deg coeff deg coeff deg coeff
9794, 95, 96mp2an 672 . . . . . . . . . . . . . . 15 deg coeff
98 unfi 7680 . . . . . . . . . . . . . . 15 deg deg coeff deg deg coeff
9991, 97, 98mp2an 672 . . . . . . . . . . . . . 14 deg deg coeff
10099a1i 11 . . . . . . . . . . . . 13 Poly deg deg coeff
101 ne0i 3741 . . . . . . . . . . . . . . 15 deg deg deg coeff deg deg coeff
10222, 101ax-mp 5 . . . . . . . . . . . . . 14 deg deg coeff
103102a1i 11 . . . . . . . . . . . . 13 Poly deg deg coeff
104 xrltso 11219 . . . . . . . . . . . . . 14
105 fisupcl 7818 . . . . . . . . . . . . . 14 deg deg coeff deg deg coeff deg deg coeff deg deg coeff deg deg coeff
106104, 105mpan 670 . . . . . . . . . . . . 13 deg deg coeff deg deg coeff deg deg coeff deg deg coeff deg deg coeff
107100, 103, 18, 106syl3anc 1219 . . . . . . . . . . . 12 Poly deg deg coeff deg deg coeff
10814, 107sseldd 3455 . . . . . . . . . . 11 Poly deg deg coeff
1091083adant2 1007 . . . . . . . . . 10 Poly deg deg coeff
110 eqidd 2452 . . . . . . . . . 10 Poly Poly deg deg deg coeff coeff deg deg coeff Poly deg deg deg coeff coeff deg deg coeff
111 breq2 4394 . . . . . . . . . . . . . . . 16 deg deg coeff deg deg deg deg coeff
112 breq2 4394 . . . . . . . . . . . . . . . . 17 deg deg coeff coeff coeff deg deg coeff
113112ralbidv 2839 . . . . . . . . . . . . . . . 16 deg deg coeff coeff coeff deg deg coeff
114111, 1133anbi23d 1293 . . . . . . . . . . . . . . 15 deg deg coeff deg coeff deg deg deg coeff coeff deg deg coeff
115114rabbidv 3060 . . . . . . . . . . . . . 14 deg deg coeff Poly deg coeff Poly deg deg deg coeff coeff deg deg coeff
116115rexeqdv 3020 . . . . . . . . . . . . 13 deg deg coeff Poly deg coeff Poly deg deg deg coeff coeff deg deg coeff
117116rabbidv 3060 . . . . . . . . . . . 12 deg deg coeff Poly deg coeff Poly deg deg deg coeff coeff deg deg coeff
118117eqeq2d 2465 . . . . . . . . . . 11 deg deg coeff Poly deg deg deg coeff coeff deg deg coeff Poly deg coeff Poly deg deg deg coeff coeff deg deg coeff Poly deg deg deg coeff coeff deg deg coeff
119118rspcev 3169 . . . . . . . . . 10 deg deg coeff Poly deg deg deg coeff coeff deg deg coeff Poly deg deg deg coeff coeff deg deg coeff Poly deg deg deg coeff coeff deg deg coeff Poly deg coeff
120109, 110, 119syl2anc 661 . . . . . . . . 9 Poly Poly deg deg deg coeff coeff deg deg coeff Poly deg coeff
121 cnex 9464 . . . . . . . . . . 11
122121rabex 4541 . . . . . . . . . 10 Poly deg deg deg coeff coeff deg deg coeff
123 eleq2 2524 . . . . . . . . . . 11 Poly deg deg deg coeff coeff deg deg coeff Poly deg deg deg coeff coeff deg deg coeff
124 eqeq1 2455 . . . . . . . . . . . 12 Poly deg deg deg coeff coeff deg deg coeff Poly deg coeff Poly deg deg deg coeff coeff deg deg coeff Poly deg coeff
125124rexbidv 2844 . . . . . . . . . . 11 Poly deg deg deg coeff coeff deg deg coeff Poly deg coeff Poly deg deg deg coeff coeff deg deg coeff Poly deg coeff
126123, 125anbi12d 710 . . . . . . . . . 10 Poly deg deg deg coeff coeff deg deg coeff Poly deg coeff Poly deg deg deg coeff coeff deg deg coeff Poly deg deg deg coeff coeff deg deg coeff Poly deg coeff
127122, 126spcev 3160 . . . . . . . . 9 Poly deg deg deg coeff coeff deg deg coeff Poly deg deg deg coeff coeff deg deg coeff Poly deg coeff Poly deg coeff
12890, 120, 127syl2anc 661 . . . . . . . 8 Poly Poly deg coeff
1291283exp 1187 . . . . . . 7 Poly Poly deg coeff
130129rexlimiv 2931 . . . . . 6 Poly Poly deg coeff
131130impcom 430 . . . . 5 Poly Poly deg coeff
132 eleq2 2524 . . . . . . . . 9 Poly deg coeff Poly deg coeff
13387rexbidv 2844 . . . . . . . . . . 11 Poly deg coeff Poly deg coeff
134133elrab 3214 . . . . . . . . . 10 Poly deg coeff Poly deg coeff
135 simp1 988 . . . . . . . . . . . . . . 15 deg coeff
136135anim2i 569 . . . . . . . . . . . . . 14 Poly deg coeff Poly
13771breq1d 4400 . . . . . . . . . . . . . . . 16 deg deg
13875breq1d 4400 . . . . . . . . . . . . . . . . 17 coeff coeff
139138ralbidv 2839 . . . . . . . . . . . . . . . 16 coeff coeff
14070, 137, 1393anbi123d 1290 . . . . . . . . . . . . . . 15 deg coeff deg coeff
141140elrab 3214 . . . . . . . . . . . . . 14 Poly deg coeff Poly deg coeff
142 eldifsn 4098 . . . . . . . . . . . . . 14 Poly Poly
143136, 141, 1423imtr4i 266 . . . . . . . . . . . . 13 Poly deg coeff Poly
144143ssriv 3458 . . . . . . . . . . . 12 Poly deg coeff Poly
145 ssrexv 3515 . . . . . . . . . . . . 13 Poly deg coeff Poly Poly deg coeff Poly
14683cbvrexv 3044 . . . . . . . . . . . . 13 Poly Poly
147145, 146syl6ib 226 . . . . . . . . . . . 12 Poly deg coeff Poly Poly deg coeff Poly
148144, 147ax-mp 5 . . . . . . . . . . 11 Poly deg coeff Poly
149148anim2i 569 . . . . . . . . . 10 Poly deg coeff Poly
150134, 149sylbi 195 . . . . . . . . 9 Poly deg coeff Poly
151132, 150syl6bi 228 . . . . . . . 8 Poly deg coeff Poly
152151rexlimivw 2933 . . . . . . 7 Poly deg coeff Poly
153152impcom 430 . . . . . 6 Poly deg coeff Poly
154153exlimiv 1689 . . . . 5 Poly deg coeff Poly
155131, 154impbii 188 . . . 4 Poly Poly deg coeff
156 elaa 21898 . . . 4 Poly
157 eluniab 4200 . . . 4 Poly deg coeff Poly deg coeff
158155, 156, 1573bitr4i 277 . . 3 Poly deg coeff
159158eqriv 2447 . 2 Poly deg coeff
160 aannenlem.a . . . 4 Poly deg coeff
161160rnmpt 5183 . . 3 Poly deg coeff
162161unieqi 4198 . 2 Poly deg coeff
163159, 162eqtr4i 2483 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 369   w3a 965   wceq 1370  wex 1587   wcel 1758  cab 2436   wne 2644  wral 2795  wrex 2796  crab 2799   cdif 3423   cun 3424   wss 3426  c0 3735  csn 3975  cpr 3977  cuni 4189   class class class wbr 4390   cmpt 4448   wor 4738   crn 4939  wf 5512  cfv 5516  (class class class)co 6190  cfn 7410  csup 7791  cc 9381  cr 9382  cc0 9383  cxr 9518   clt 9519   cle 9520  cn0 10680  cz 10747  cfz 11538  cabs 12825  c0p 21263  Polycply 21768  coeffccoe 21770  degcdgr 21771  caa 21896 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-rep 4501  ax-sep 4511  ax-nul 4519  ax-pow 4568  ax-pr 4629  ax-un 6472  ax-inf2 7948  ax-cnex 9439  ax-resscn 9440  ax-1cn 9441  ax-icn 9442  ax-addcl 9443  ax-addrcl 9444  ax-mulcl 9445  ax-mulrcl 9446  ax-mulcom 9447  ax-addass 9448  ax-mulass 9449  ax-distr 9450  ax-i2m1 9451  ax-1ne0 9452  ax-1rid 9453  ax-rnegex 9454  ax-rrecex 9455  ax-cnre 9456  ax-pre-lttri 9457  ax-pre-lttrn 9458  ax-pre-ltadd 9459  ax-pre-mulgt0 9460  ax-pre-sup 9461  ax-addf 9462 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-fal 1376  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-nel 2647  df-ral 2800  df-rex 2801  df-reu 2802  df-rmo 2803  df-rab 2804  df-v 3070  df-sbc 3285  df-csb 3387  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-pss 3442  df-nul 3736  df-if 3890  df-pw 3960  df-sn 3976  df-pr 3978  df-tp 3980  df-op 3982  df-uni 4190  df-int 4227  df-iun 4271  df-br 4391  df-opab 4449  df-mpt 4450  df-tr 4484  df-eprel 4730  df-id 4734  df-po 4739  df-so 4740  df-fr 4777  df-se 4778  df-we 4779  df-ord 4820  df-on 4821  df-lim 4822  df-suc 4823  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-rn 4949  df-res 4950  df-ima 4951  df-iota 5479  df-fun 5518  df-fn 5519  df-f 5520  df-f1 5521  df-fo 5522  df-f1o 5523  df-fv 5524  df-isom 5525  df-riota 6151  df-ov 6193  df-oprab 6194  df-mpt2 6195  df-of 6420  df-om 6577  df-1st 6677  df-2nd 6678  df-recs 6932  df-rdg 6966  df-1o 7020  df-oadd 7024  df-er 7201  df-map 7316  df-pm 7317  df-en 7411  df-dom 7412  df-sdom 7413  df-fin 7414  df-sup 7792  df-oi 7825  df-card 8210  df-pnf 9521  df-mnf 9522  df-xr 9523  df-ltxr 9524  df-le 9525  df-sub 9698  df-neg 9699  df-div 10095  df-nn 10424  df-2 10481  df-3 10482  df-n0 10681  df-z 10748  df-uz 10963  df-rp 11093  df-fz 11539  df-fzo 11650  df-fl 11743  df-seq 11908  df-exp 11967  df-hash 12205  df-cj 12690  df-re 12691  df-im 12692  df-sqr 12826  df-abs 12827  df-clim 13068  df-rlim 13069  df-sum 13266  df-0p 21264  df-ply 21772  df-coe 21774  df-dgr 21775  df-aa 21897 This theorem is referenced by:  aannenlem3  21912
 Copyright terms: Public domain W3C validator