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

Theorem aannenlem2 19725
 Description: Lemma for aannen 19727. (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 957 . . . . . . . . . 10 Poly
2 eldifi 3311 . . . . . . . . . . . . . 14 Poly Poly
32adantr 451 . . . . . . . . . . . . 13 Poly Poly
433adant2 974 . . . . . . . . . . . 12 Poly Poly
5 eldifsni 3763 . . . . . . . . . . . . . . 15 Poly
65adantr 451 . . . . . . . . . . . . . 14 Poly
7 0nn0 9996 . . . . . . . . . . . . . . . . . 18
8 dgrcl 19631 . . . . . . . . . . . . . . . . . . 19 Poly deg
93, 8syl 15 . . . . . . . . . . . . . . . . . 18 Poly deg
10 prssi 3787 . . . . . . . . . . . . . . . . . 18 deg deg
117, 9, 10sylancr 644 . . . . . . . . . . . . . . . . 17 Poly deg
12 ssrab2 3271 . . . . . . . . . . . . . . . . . 18 deg coeff
1312a1i 10 . . . . . . . . . . . . . . . . 17 Poly deg coeff
1411, 13unssd 3364 . . . . . . . . . . . . . . . 16 Poly deg deg coeff
15 nn0ssre 9985 . . . . . . . . . . . . . . . . 17
16 ressxr 8892 . . . . . . . . . . . . . . . . 17
1715, 16sstri 3201 . . . . . . . . . . . . . . . 16
1814, 17syl6ss 3204 . . . . . . . . . . . . . . 15 Poly deg deg coeff
19 fvex 5555 . . . . . . . . . . . . . . . . 17 deg
2019prid2 3748 . . . . . . . . . . . . . . . 16 deg deg
21 elun1 3355 . . . . . . . . . . . . . . . 16 deg deg deg deg deg coeff
2220, 21ax-mp 8 . . . . . . . . . . . . . . 15 deg deg deg coeff
23 supxrub 10659 . . . . . . . . . . . . . . 15 deg deg coeff deg deg deg coeff deg deg deg coeff
2418, 22, 23sylancl 643 . . . . . . . . . . . . . 14 Poly deg deg deg coeff
2518adantr 451 . . . . . . . . . . . . . . . 16 Poly deg deg coeff
26 fveq2 5541 . . . . . . . . . . . . . . . . . . . 20 coeff coeff
27 abs0 11786 . . . . . . . . . . . . . . . . . . . 20
2826, 27syl6eq 2344 . . . . . . . . . . . . . . . . . . 19 coeff coeff
29 c0ex 8848 . . . . . . . . . . . . . . . . . . . . 21
3029prid1 3747 . . . . . . . . . . . . . . . . . . . 20 deg
31 elun1 3355 . . . . . . . . . . . . . . . . . . . 20 deg deg deg coeff
3230, 31ax-mp 8 . . . . . . . . . . . . . . . . . . 19 deg deg coeff
3328, 32syl6eqel 2384 . . . . . . . . . . . . . . . . . 18 coeff coeff deg deg coeff
3433adantl 452 . . . . . . . . . . . . . . . . 17 Poly coeff coeff deg deg coeff
35 0z 10051 . . . . . . . . . . . . . . . . . . . . . . 23
36 eqid 2296 . . . . . . . . . . . . . . . . . . . . . . . 24 coeff coeff
3736coef2 19629 . . . . . . . . . . . . . . . . . . . . . . 23 Poly coeff
383, 35, 37sylancl 643 . . . . . . . . . . . . . . . . . . . . . 22 Poly coeff
3938ffvelrnda 5681 . . . . . . . . . . . . . . . . . . . . 21 Poly coeff
40 nn0abscl 11813 . . . . . . . . . . . . . . . . . . . . 21 coeff coeff
4139, 40syl 15 . . . . . . . . . . . . . . . . . . . 20 Poly coeff
4241adantr 451 . . . . . . . . . . . . . . . . . . 19 Poly coeff coeff
43 simplr 731 . . . . . . . . . . . . . . . . . . . . 21 Poly coeff
449ad2antrr 706 . . . . . . . . . . . . . . . . . . . . 21 Poly coeff deg
453ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . 22 Poly coeff Poly
46 simpr 447 . . . . . . . . . . . . . . . . . . . . . 22 Poly coeff coeff
47 eqid 2296 . . . . . . . . . . . . . . . . . . . . . . 23 deg deg
4836, 47dgrub 19632 . . . . . . . . . . . . . . . . . . . . . 22 Poly coeff deg
4945, 43, 46, 48syl3anc 1182 . . . . . . . . . . . . . . . . . . . . 21 Poly coeff deg
50 elfz2nn0 10837 . . . . . . . . . . . . . . . . . . . . 21 deg deg deg
5143, 44, 49, 50syl3anbrc 1136 . . . . . . . . . . . . . . . . . . . 20 Poly coeff deg
52 eqid 2296 . . . . . . . . . . . . . . . . . . . 20 coeff coeff
53 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . 23 coeff coeff
5453fveq2d 5545 . . . . . . . . . . . . . . . . . . . . . 22 coeff coeff
5554eqeq2d 2307 . . . . . . . . . . . . . . . . . . . . 21 coeff coeff coeff coeff
5655rspcev 2897 . . . . . . . . . . . . . . . . . . . 20 deg coeff coeff degcoeff coeff
5751, 52, 56sylancl 643 . . . . . . . . . . . . . . . . . . 19 Poly coeff degcoeff coeff
58 eqeq1 2302 . . . . . . . . . . . . . . . . . . . . 21 coeff coeff coeff coeff
5958rexbidv 2577 . . . . . . . . . . . . . . . . . . . 20 coeff deg coeff degcoeff coeff
6059elrab 2936 . . . . . . . . . . . . . . . . . . 19 coeff deg coeff coeff degcoeff coeff
6142, 57, 60sylanbrc 645 . . . . . . . . . . . . . . . . . 18 Poly coeff coeff deg coeff
62 elun2 3356 . . . . . . . . . . . . . . . . . 18 coeff deg coeff coeff deg deg coeff
6361, 62syl 15 . . . . . . . . . . . . . . . . 17 Poly coeff coeff deg deg coeff
6434, 63pm2.61dane 2537 . . . . . . . . . . . . . . . 16 Poly coeff deg deg coeff
65 supxrub 10659 . . . . . . . . . . . . . . . 16 deg deg coeff coeff deg deg coeff coeff deg deg coeff
6625, 64, 65syl2anc 642 . . . . . . . . . . . . . . 15 Poly coeff deg deg coeff
6766ralrimiva 2639 . . . . . . . . . . . . . 14 Poly coeff deg deg coeff
686, 24, 673jca 1132 . . . . . . . . . . . . 13 Poly deg deg deg coeff coeff deg deg coeff
69683adant2 974 . . . . . . . . . . . 12 Poly deg deg deg coeff coeff deg deg coeff
70 neeq1 2467 . . . . . . . . . . . . . 14
71 fveq2 5541 . . . . . . . . . . . . . . 15 deg deg
7271breq1d 4049 . . . . . . . . . . . . . 14 deg deg deg coeff deg deg deg coeff
73 fveq2 5541 . . . . . . . . . . . . . . . . . 18 coeff coeff
7473fveq1d 5543 . . . . . . . . . . . . . . . . 17 coeff coeff
7574fveq2d 5545 . . . . . . . . . . . . . . . 16 coeff coeff
7675breq1d 4049 . . . . . . . . . . . . . . 15 coeff deg deg coeff coeff deg deg coeff
7776ralbidv 2576 . . . . . . . . . . . . . 14 coeff deg deg coeff coeff deg deg coeff
7870, 72, 773anbi123d 1252 . . . . . . . . . . . . 13 deg deg deg coeff coeff deg deg coeff deg deg deg coeff coeff deg deg coeff
7978elrab 2936 . . . . . . . . . . . 12 Poly deg deg deg coeff coeff deg deg coeff Poly deg deg deg coeff coeff deg deg coeff
804, 69, 79sylanbrc 645 . . . . . . . . . . 11 Poly Poly deg deg deg coeff coeff deg deg coeff
81 simp2 956 . . . . . . . . . . 11 Poly
82 fveq1 5540 . . . . . . . . . . . . 13
8382eqeq1d 2304 . . . . . . . . . . . 12
8483rspcev 2897 . . . . . . . . . . 11 Poly deg deg deg coeff coeff deg deg coeff Poly deg deg deg coeff coeff deg deg coeff
8580, 81, 84syl2anc 642 . . . . . . . . . 10 Poly Poly deg deg deg coeff coeff deg deg coeff
86 fveq2 5541 . . . . . . . . . . . . 13
8786eqeq1d 2304 . . . . . . . . . . . 12
8887rexbidv 2577 . . . . . . . . . . 11 Poly deg deg deg coeff coeff deg deg coeff Poly deg deg deg coeff coeff deg deg coeff
8988elrab 2936 . . . . . . . . . 10 Poly deg deg deg coeff coeff deg deg coeff Poly deg deg deg coeff coeff deg deg coeff
901, 85, 89sylanbrc 645 . . . . . . . . 9 Poly Poly deg deg deg coeff coeff deg deg coeff
91 prfi 7147 . . . . . . . . . . . . . . 15 deg
92 fzfi 11050 . . . . . . . . . . . . . . . . 17 deg
93 abrexfi 7172 . . . . . . . . . . . . . . . . 17 deg deg coeff
9492, 93ax-mp 8 . . . . . . . . . . . . . . . 16 deg coeff
95 rabssab 3272 . . . . . . . . . . . . . . . 16 deg coeff deg coeff
96 ssfi 7099 . . . . . . . . . . . . . . . 16 deg coeff deg coeff deg coeff deg coeff
9794, 95, 96mp2an 653 . . . . . . . . . . . . . . 15 deg coeff
98 unfi 7140 . . . . . . . . . . . . . . 15 deg deg coeff deg deg coeff
9991, 97, 98mp2an 653 . . . . . . . . . . . . . 14 deg deg coeff
10099a1i 10 . . . . . . . . . . . . 13 Poly deg deg coeff
101 ne0i 3474 . . . . . . . . . . . . . . 15 deg deg deg coeff deg deg coeff
10222, 101ax-mp 8 . . . . . . . . . . . . . 14 deg deg coeff
103102a1i 10 . . . . . . . . . . . . 13 Poly deg deg coeff
104 xrltso 10491 . . . . . . . . . . . . . 14
105 fisupcl 7234 . . . . . . . . . . . . . 14 deg deg coeff deg deg coeff deg deg coeff deg deg coeff deg deg coeff
106104, 105mpan 651 . . . . . . . . . . . . 13 deg deg coeff deg deg coeff deg deg coeff deg deg coeff deg deg coeff
107100, 103, 18, 106syl3anc 1182 . . . . . . . . . . . 12 Poly deg deg coeff deg deg coeff
10814, 107sseldd 3194 . . . . . . . . . . 11 Poly deg deg coeff
1091083adant2 974 . . . . . . . . . 10 Poly deg deg coeff
110 eqidd 2297 . . . . . . . . . 10 Poly Poly deg deg deg coeff coeff deg deg coeff Poly deg deg deg coeff coeff deg deg coeff
111 breq2 4043 . . . . . . . . . . . . . . . 16 deg deg coeff deg deg deg deg coeff
112 breq2 4043 . . . . . . . . . . . . . . . . 17 deg deg coeff coeff coeff deg deg coeff
113112ralbidv 2576 . . . . . . . . . . . . . . . 16 deg deg coeff coeff coeff deg deg coeff
114111, 1133anbi23d 1255 . . . . . . . . . . . . . . 15 deg deg coeff deg coeff deg deg deg coeff coeff deg deg coeff
115114rabbidv 2793 . . . . . . . . . . . . . 14 deg deg coeff Poly deg coeff Poly deg deg deg coeff coeff deg deg coeff
116115rexeqdv 2756 . . . . . . . . . . . . 13 deg deg coeff Poly deg coeff Poly deg deg deg coeff coeff deg deg coeff
117116rabbidv 2793 . . . . . . . . . . . 12 deg deg coeff Poly deg coeff Poly deg deg deg coeff coeff deg deg coeff
118117eqeq2d 2307 . . . . . . . . . . 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 2897 . . . . . . . . . 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 642 . . . . . . . . 9 Poly Poly deg deg deg coeff coeff deg deg coeff Poly deg coeff
121 cnex 8834 . . . . . . . . . . 11
122121rabex 4181 . . . . . . . . . 10 Poly deg deg deg coeff coeff deg deg coeff
123 eleq2 2357 . . . . . . . . . . 11 Poly deg deg deg coeff coeff deg deg coeff Poly deg deg deg coeff coeff deg deg coeff
124 eqeq1 2302 . . . . . . . . . . . 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 2577 . . . . . . . . . . 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 691 . . . . . . . . . 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 2888 . . . . . . . . 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 642 . . . . . . . 8 Poly Poly deg coeff
1291283exp 1150 . . . . . . 7 Poly Poly deg coeff
130129rexlimiv 2674 . . . . . 6 Poly Poly deg coeff
131130impcom 419 . . . . 5 Poly Poly deg coeff
132 eleq2 2357 . . . . . . . . 9 Poly deg coeff Poly deg coeff
13387rexbidv 2577 . . . . . . . . . . 11 Poly deg coeff Poly deg coeff
134133elrab 2936 . . . . . . . . . 10 Poly deg coeff Poly deg coeff
135 simp1 955 . . . . . . . . . . . . . . 15 deg coeff
136135anim2i 552 . . . . . . . . . . . . . 14 Poly deg coeff Poly
13771breq1d 4049 . . . . . . . . . . . . . . . 16 deg deg
13875breq1d 4049 . . . . . . . . . . . . . . . . 17 coeff coeff
139138ralbidv 2576 . . . . . . . . . . . . . . . 16 coeff coeff
14070, 137, 1393anbi123d 1252 . . . . . . . . . . . . . . 15 deg coeff deg coeff
141140elrab 2936 . . . . . . . . . . . . . 14 Poly deg coeff Poly deg coeff
142 eldifsn 3762 . . . . . . . . . . . . . 14 Poly Poly
143136, 141, 1423imtr4i 257 . . . . . . . . . . . . 13 Poly deg coeff Poly
144143ssriv 3197 . . . . . . . . . . . 12 Poly deg coeff Poly
145 ssrexv 3251 . . . . . . . . . . . . 13 Poly deg coeff Poly Poly deg coeff Poly
14683cbvrexv 2778 . . . . . . . . . . . . 13 Poly Poly
147145, 146syl6ib 217 . . . . . . . . . . . 12 Poly deg coeff Poly Poly deg coeff Poly
148144, 147ax-mp 8 . . . . . . . . . . 11 Poly deg coeff Poly
149148anim2i 552 . . . . . . . . . 10 Poly deg coeff Poly
150134, 149sylbi 187 . . . . . . . . 9 Poly deg coeff Poly
151132, 150syl6bi 219 . . . . . . . 8 Poly deg coeff Poly
152151rexlimivw 2676 . . . . . . 7 Poly deg coeff Poly
153152impcom 419 . . . . . 6 Poly deg coeff Poly
154153exlimiv 1624 . . . . 5 Poly deg coeff Poly
155131, 154impbii 180 . . . 4 Poly Poly deg coeff
156 elaa 19712 . . . 4 Poly
157 eluniab 3855 . . . 4 Poly deg coeff Poly deg coeff
158155, 156, 1573bitr4i 268 . . 3 Poly deg coeff
159158eqriv 2293 . 2 Poly deg coeff
160 aannenlem.a . . . 4 Poly deg coeff
161160rnmpt 4941 . . 3 Poly deg coeff
162161unieqi 3853 . 2 Poly deg coeff
163159, 162eqtr4i 2319 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 358   w3a 934  wex 1531   wceq 1632   wcel 1696  cab 2282   wne 2459  wral 2556  wrex 2557  crab 2560   cdif 3162   cun 3163   wss 3165  c0 3468  csn 3653  cpr 3654  cuni 3843   class class class wbr 4039   cmpt 4093   wor 4329   crn 4706  wf 5267  cfv 5271  (class class class)co 5874  cfn 6879  csup 7209  cc 8751  cr 8752  cc0 8753  cxr 8882   clt 8883   cle 8884  cn0 9981  cz 10040  cfz 10798  cabs 11735  c0p 19040  Polycply 19582  coeffccoe 19584  degcdgr 19585  caa 19710 This theorem is referenced by:  aannenlem3  19726 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-rep 4147  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528  ax-inf2 7358  ax-cnex 8809  ax-resscn 8810  ax-1cn 8811  ax-icn 8812  ax-addcl 8813  ax-addrcl 8814  ax-mulcl 8815  ax-mulrcl 8816  ax-mulcom 8817  ax-addass 8818  ax-mulass 8819  ax-distr 8820  ax-i2m1 8821  ax-1ne0 8822  ax-1rid 8823  ax-rnegex 8824  ax-rrecex 8825  ax-cnre 8826  ax-pre-lttri 8827  ax-pre-lttrn 8828  ax-pre-ltadd 8829  ax-pre-mulgt0 8830  ax-pre-sup 8831  ax-addf 8832 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-nel 2462  df-ral 2561  df-rex 2562  df-reu 2563  df-rmo 2564  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pss 3181  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-tp 3661  df-op 3662  df-uni 3844  df-int 3879  df-iun 3923  df-br 4040  df-opab 4094  df-mpt 4095  df-tr 4130  df-eprel 4321  df-id 4325  df-po 4330  df-so 4331  df-fr 4368  df-se 4369  df-we 4370  df-ord 4411  df-on 4412  df-lim 4413  df-suc 4414  df-om 4673  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-isom 5280  df-ov 5877  df-oprab 5878  df-mpt2 5879  df-of 6094  df-1st 6138  df-2nd 6139  df-riota 6320  df-recs 6404  df-rdg 6439  df-1o 6495  df-oadd 6499  df-er 6676  df-map 6790  df-pm 6791  df-en 6880  df-dom 6881  df-sdom 6882  df-fin 6883  df-sup 7210  df-oi 7241  df-card 7588  df-pnf 8885  df-mnf 8886  df-xr 8887  df-ltxr 8888  df-le 8889  df-sub 9055  df-neg 9056  df-div 9440  df-nn 9763  df-2 9820  df-3 9821  df-n0 9982  df-z 10041  df-uz 10247  df-rp 10371  df-fz 10799  df-fzo 10887  df-fl 10941  df-seq 11063  df-exp 11121  df-hash 11354  df-cj 11600  df-re 11601  df-im 11602  df-sqr 11736  df-abs 11737  df-clim 11978  df-rlim 11979  df-sum 12175  df-0p 19041  df-ply 19586  df-coe 19588  df-dgr 19589  df-aa 19711
 Copyright terms: Public domain W3C validator