Step | Hyp | Ref
| Expression |
1 | | simp3 1063 |
. . . . . . . . . 10
Poly |
2 | | eldifi 3732 |
. . . . . . . . . . . . . 14
Poly
Poly |
3 | 2 | adantr 481 |
. . . . . . . . . . . . 13
Poly Poly |
4 | 3 | 3adant2 1080 |
. . . . . . . . . . . 12
Poly Poly |
5 | | eldifsni 4320 |
. . . . . . . . . . . . . . 15
Poly
|
6 | 5 | adantr 481 |
. . . . . . . . . . . . . 14
Poly |
7 | | 0nn0 11307 |
. . . . . . . . . . . . . . . . . 18
|
8 | | dgrcl 23989 |
. . . . . . . . . . . . . . . . . . 19
Poly deg |
9 | 3, 8 | syl 17 |
. . . . . . . . . . . . . . . . . 18
Poly deg |
10 | | prssi 4353 |
. . . . . . . . . . . . . . . . . 18
deg deg |
11 | 7, 9, 10 | sylancr 695 |
. . . . . . . . . . . . . . . . 17
Poly deg |
12 | | ssrab2 3687 |
. . . . . . . . . . . . . . . . . 18
deg coeff |
13 | 12 | a1i 11 |
. . . . . . . . . . . . . . . . 17
Poly
deg coeff |
14 | 11, 13 | unssd 3789 |
. . . . . . . . . . . . . . . 16
Poly deg
deg coeff
|
15 | | nn0ssre 11296 |
. . . . . . . . . . . . . . . . 17
|
16 | | ressxr 10083 |
. . . . . . . . . . . . . . . . 17
|
17 | 15, 16 | sstri 3612 |
. . . . . . . . . . . . . . . 16
|
18 | 14, 17 | syl6ss 3615 |
. . . . . . . . . . . . . . 15
Poly deg
deg coeff
|
19 | | fvex 6201 |
. . . . . . . . . . . . . . . . 17
deg |
20 | 19 | prid2 4298 |
. . . . . . . . . . . . . . . 16
deg deg |
21 | | elun1 3780 |
. . . . . . . . . . . . . . . 16
deg deg deg deg
deg coeff |
22 | 20, 21 | ax-mp 5 |
. . . . . . . . . . . . . . 15
deg deg
deg coeff |
23 | | supxrub 12154 |
. . . . . . . . . . . . . . 15
deg
deg coeff
deg deg
deg coeff deg deg
deg coeff |
24 | 18, 22, 23 | sylancl 694 |
. . . . . . . . . . . . . 14
Poly deg
deg
deg coeff |
25 | 18 | adantr 481 |
. . . . . . . . . . . . . . . 16
Poly
deg
deg coeff
|
26 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
coeff coeff |
27 | | abs0 14025 |
. . . . . . . . . . . . . . . . . . . 20
|
28 | 26, 27 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . 19
coeff coeff |
29 | | c0ex 10034 |
. . . . . . . . . . . . . . . . . . . . 21
|
30 | 29 | prid1 4297 |
. . . . . . . . . . . . . . . . . . . 20
deg |
31 | | elun1 3780 |
. . . . . . . . . . . . . . . . . . . 20
deg deg
deg coeff |
32 | 30, 31 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
deg
deg coeff |
33 | 28, 32 | syl6eqel 2709 |
. . . . . . . . . . . . . . . . . 18
coeff coeff deg
deg coeff |
34 | 33 | adantl 482 |
. . . . . . . . . . . . . . . . 17
Poly coeff
coeff deg
deg coeff |
35 | | 0z 11388 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
36 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . 24
coeff coeff |
37 | 36 | coef2 23987 |
. . . . . . . . . . . . . . . . . . . . . . 23
Poly
coeff |
38 | 3, 35, 37 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . 22
Poly coeff |
39 | 38 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . 21
Poly
coeff |
40 | | nn0abscl 14052 |
. . . . . . . . . . . . . . . . . . . . 21
coeff coeff |
41 | 39, 40 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
Poly
coeff |
42 | 41 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
Poly coeff
coeff |
43 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . 21
Poly coeff
|
44 | 9 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
Poly coeff
deg |
45 | 3 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
Poly coeff
Poly |
46 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . 22
Poly coeff
coeff |
47 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . 23
deg deg |
48 | 36, 47 | dgrub 23990 |
. . . . . . . . . . . . . . . . . . . . . 22
Poly
coeff deg |
49 | 45, 43, 46, 48 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . 21
Poly coeff
deg |
50 | | elfz2nn0 12431 |
. . . . . . . . . . . . . . . . . . . . 21
deg
deg deg |
51 | 43, 44, 49, 50 | syl3anbrc 1246 |
. . . . . . . . . . . . . . . . . . . 20
Poly coeff
deg |
52 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
coeff coeff |
53 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
coeff coeff |
54 | 53 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . 22
coeff coeff |
55 | 54 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . 21
coeff coeff
coeff coeff |
56 | 55 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . . 20
deg coeff coeff
degcoeff coeff |
57 | 51, 52, 56 | sylancl 694 |
. . . . . . . . . . . . . . . . . . 19
Poly coeff
degcoeff coeff |
58 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . 21
coeff coeff
coeff coeff |
59 | 58 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . . . 20
coeff deg coeff
degcoeff coeff |
60 | 59 | elrab 3363 |
. . . . . . . . . . . . . . . . . . 19
coeff
deg coeff coeff
degcoeff coeff |
61 | 42, 57, 60 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . 18
Poly coeff
coeff
deg coeff |
62 | | elun2 3781 |
. . . . . . . . . . . . . . . . . 18
coeff
deg coeff coeff deg
deg coeff |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . . . . . . 17
Poly coeff
coeff deg
deg coeff |
64 | 34, 63 | pm2.61dane 2881 |
. . . . . . . . . . . . . . . 16
Poly
coeff deg
deg coeff |
65 | | supxrub 12154 |
. . . . . . . . . . . . . . . 16
deg
deg coeff
coeff deg
deg coeff coeff deg
deg coeff |
66 | 25, 64, 65 | syl2anc 693 |
. . . . . . . . . . . . . . 15
Poly
coeff deg
deg coeff |
67 | 66 | ralrimiva 2966 |
. . . . . . . . . . . . . 14
Poly coeff deg
deg coeff |
68 | 6, 24, 67 | 3jca 1242 |
. . . . . . . . . . . . 13
Poly deg deg
deg coeff coeff deg
deg coeff |
69 | 68 | 3adant2 1080 |
. . . . . . . . . . . 12
Poly deg deg
deg coeff coeff deg
deg coeff |
70 | | neeq1 2856 |
. . . . . . . . . . . . . 14
|
71 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
deg deg |
72 | 71 | breq1d 4663 |
. . . . . . . . . . . . . 14
deg deg
deg coeff deg deg
deg coeff |
73 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
coeff coeff |
74 | 73 | fveq1d 6193 |
. . . . . . . . . . . . . . . . 17
coeff coeff |
75 | 74 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
coeff coeff |
76 | 75 | breq1d 4663 |
. . . . . . . . . . . . . . 15
coeff deg
deg coeff coeff deg
deg coeff |
77 | 76 | ralbidv 2986 |
. . . . . . . . . . . . . 14
coeff deg
deg coeff
coeff deg
deg coeff |
78 | 70, 72, 77 | 3anbi123d 1399 |
. . . . . . . . . . . . 13
deg
deg
deg coeff coeff deg
deg coeff deg deg
deg coeff coeff deg
deg coeff |
79 | 78 | elrab 3363 |
. . . . . . . . . . . 12
Poly deg deg
deg coeff coeff deg
deg coeff
Poly deg
deg
deg coeff coeff deg
deg coeff |
80 | 4, 69, 79 | sylanbrc 698 |
. . . . . . . . . . 11
Poly Poly
deg
deg
deg coeff coeff deg
deg coeff |
81 | | simp2 1062 |
. . . . . . . . . . 11
Poly |
82 | | fveq1 6190 |
. . . . . . . . . . . . 13
|
83 | 82 | eqeq1d 2624 |
. . . . . . . . . . . 12
|
84 | 83 | rspcev 3309 |
. . . . . . . . . . 11
Poly
deg deg
deg coeff coeff deg
deg coeff
Poly
deg deg
deg coeff coeff deg
deg coeff |
85 | 80, 81, 84 | syl2anc 693 |
. . . . . . . . . 10
Poly Poly
deg
deg
deg coeff coeff deg
deg coeff |
86 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
87 | 86 | eqeq1d 2624 |
. . . . . . . . . . . 12
|
88 | 87 | rexbidv 3052 |
. . . . . . . . . . 11
Poly
deg deg
deg coeff coeff deg
deg coeff Poly
deg
deg
deg coeff coeff deg
deg coeff |
89 | 88 | elrab 3363 |
. . . . . . . . . 10
Poly deg
deg
deg coeff coeff deg
deg coeff
Poly deg
deg
deg coeff coeff deg
deg coeff |
90 | 1, 85, 89 | sylanbrc 698 |
. . . . . . . . 9
Poly
Poly
deg deg
deg coeff coeff deg
deg coeff |
91 | | prfi 8235 |
. . . . . . . . . . . . . . 15
deg |
92 | | fzfi 12771 |
. . . . . . . . . . . . . . . . 17
deg |
93 | | abrexfi 8266 |
. . . . . . . . . . . . . . . . 17
deg deg coeff |
94 | 92, 93 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
deg coeff |
95 | | rabssab 3690 |
. . . . . . . . . . . . . . . 16
deg coeff deg coeff |
96 | | ssfi 8180 |
. . . . . . . . . . . . . . . 16
deg coeff
deg coeff deg coeff
deg coeff |
97 | 94, 95, 96 | mp2an 708 |
. . . . . . . . . . . . . . 15
deg coeff |
98 | | unfi 8227 |
. . . . . . . . . . . . . . 15
deg
deg coeff deg
deg coeff |
99 | 91, 97, 98 | mp2an 708 |
. . . . . . . . . . . . . 14
deg
deg coeff |
100 | 99 | a1i 11 |
. . . . . . . . . . . . 13
Poly deg
deg coeff |
101 | 22 | ne0ii 3923 |
. . . . . . . . . . . . . 14
deg
deg coeff |
102 | 101 | a1i 11 |
. . . . . . . . . . . . 13
Poly deg
deg coeff |
103 | | xrltso 11974 |
. . . . . . . . . . . . . 14
|
104 | | fisupcl 8375 |
. . . . . . . . . . . . . 14
deg
deg coeff deg
deg coeff deg
deg coeff
deg
deg coeff deg
deg coeff |
105 | 103, 104 | mpan 706 |
. . . . . . . . . . . . 13
deg
deg coeff deg
deg coeff deg
deg coeff
deg
deg coeff deg
deg coeff |
106 | 100, 102,
18, 105 | syl3anc 1326 |
. . . . . . . . . . . 12
Poly deg
deg coeff deg
deg coeff |
107 | 14, 106 | sseldd 3604 |
. . . . . . . . . . 11
Poly deg
deg coeff |
108 | 107 | 3adant2 1080 |
. . . . . . . . . 10
Poly deg
deg coeff |
109 | | eqidd 2623 |
. . . . . . . . . 10
Poly Poly deg
deg
deg coeff coeff deg
deg coeff
Poly
deg deg
deg coeff coeff deg
deg coeff |
110 | | breq2 4657 |
. . . . . . . . . . . . . . . 16
deg
deg coeff deg deg deg
deg coeff |
111 | | breq2 4657 |
. . . . . . . . . . . . . . . . 17
deg
deg coeff coeff
coeff
deg
deg coeff |
112 | 111 | ralbidv 2986 |
. . . . . . . . . . . . . . . 16
deg
deg coeff coeff coeff deg
deg coeff |
113 | 110, 112 | 3anbi23d 1402 |
. . . . . . . . . . . . . . 15
deg
deg coeff deg
coeff
deg deg
deg coeff coeff deg
deg coeff |
114 | 113 | rabbidv 3189 |
. . . . . . . . . . . . . 14
deg
deg coeff Poly deg coeff Poly
deg
deg
deg coeff coeff deg
deg coeff |
115 | 114 | rexeqdv 3145 |
. . . . . . . . . . . . 13
deg
deg coeff Poly deg
coeff Poly
deg
deg
deg coeff coeff deg
deg coeff |
116 | 115 | rabbidv 3189 |
. . . . . . . . . . . 12
deg
deg coeff Poly deg
coeff
Poly
deg deg
deg coeff coeff deg
deg coeff |
117 | 116 | eqeq2d 2632 |
. . . . . . . . . . 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 |
118 | 117 | rspcev 3309 |
. . . . . . . . . 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 |
119 | 108, 109,
118 | syl2anc 693 |
. . . . . . . . 9
Poly
Poly
deg deg
deg coeff coeff deg
deg coeff
Poly
deg coeff |
120 | | cnex 10017 |
. . . . . . . . . . 11
|
121 | 120 | rabex 4813 |
. . . . . . . . . 10
Poly deg deg
deg coeff coeff deg
deg coeff |
122 | | eleq2 2690 |
. . . . . . . . . . 11
Poly deg
deg
deg coeff coeff deg
deg coeff
Poly
deg deg
deg coeff coeff deg
deg coeff |
123 | | eqeq1 2626 |
. . . . . . . . . . . 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 |
124 | 123 | rexbidv 3052 |
. . . . . . . . . . 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 |
125 | 122, 124 | anbi12d 747 |
. . . . . . . . . 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 |
126 | 121, 125 | spcev 3300 |
. . . . . . . . 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 |
127 | 90, 119, 126 | syl2anc 693 |
. . . . . . . 8
Poly
Poly
deg
coeff |
128 | 127 | 3exp 1264 |
. . . . . . 7
Poly
Poly
deg coeff |
129 | 128 | rexlimiv 3027 |
. . . . . 6
Poly
Poly
deg
coeff |
130 | 129 | impcom 446 |
. . . . 5
Poly
Poly
deg
coeff |
131 | | eleq2 2690 |
. . . . . . . . 9
Poly deg
coeff
Poly
deg coeff |
132 | 87 | rexbidv 3052 |
. . . . . . . . . . 11
Poly
deg coeff Poly
deg
coeff |
133 | 132 | elrab 3363 |
. . . . . . . . . 10
Poly deg
coeff
Poly deg
coeff |
134 | | simp1 1061 |
. . . . . . . . . . . . . . 15
deg
coeff
|
135 | 134 | anim2i 593 |
. . . . . . . . . . . . . 14
Poly
deg
coeff Poly
|
136 | 71 | breq1d 4663 |
. . . . . . . . . . . . . . . 16
deg deg |
137 | 75 | breq1d 4663 |
. . . . . . . . . . . . . . . . 17
coeff coeff |
138 | 137 | ralbidv 2986 |
. . . . . . . . . . . . . . . 16
coeff coeff |
139 | 70, 136, 138 | 3anbi123d 1399 |
. . . . . . . . . . . . . . 15
deg
coeff deg coeff |
140 | 139 | elrab 3363 |
. . . . . . . . . . . . . 14
Poly deg coeff
Poly deg
coeff |
141 | | eldifsn 4317 |
. . . . . . . . . . . . . 14
Poly
Poly
|
142 | 135, 140,
141 | 3imtr4i 281 |
. . . . . . . . . . . . 13
Poly deg coeff Poly |
143 | 142 | ssriv 3607 |
. . . . . . . . . . . 12
Poly
deg coeff Poly |
144 | | ssrexv 3667 |
. . . . . . . . . . . . 13
Poly
deg
coeff Poly
Poly deg coeff
Poly |
145 | 83 | cbvrexv 3172 |
. . . . . . . . . . . . 13
Poly
Poly |
146 | 144, 145 | syl6ib 241 |
. . . . . . . . . . . 12
Poly
deg
coeff Poly
Poly deg coeff
Poly |
147 | 143, 146 | ax-mp 5 |
. . . . . . . . . . 11
Poly
deg coeff
Poly |
148 | 147 | anim2i 593 |
. . . . . . . . . 10
Poly
deg coeff Poly |
149 | 133, 148 | sylbi 207 |
. . . . . . . . 9
Poly deg
coeff Poly |
150 | 131, 149 | syl6bi 243 |
. . . . . . . 8
Poly deg
coeff Poly |
151 | 150 | rexlimivw 3029 |
. . . . . . 7
Poly
deg
coeff Poly |
152 | 151 | impcom 446 |
. . . . . 6
Poly
deg
coeff Poly |
153 | 152 | exlimiv 1858 |
. . . . 5
Poly
deg coeff Poly |
154 | 130, 153 | impbii 199 |
. . . 4
Poly
Poly
deg coeff |
155 | | elaa 24071 |
. . . 4
Poly |
156 | | eluniab 4447 |
. . . 4
Poly
deg coeff
Poly
deg coeff |
157 | 154, 155,
156 | 3bitr4i 292 |
. . 3
Poly
deg
coeff |
158 | 157 | eqriv 2619 |
. 2
Poly
deg
coeff |
159 | | aannenlem.a |
. . . 4
Poly
deg
coeff |
160 | 159 | rnmpt 5371 |
. . 3
Poly
deg
coeff |
161 | 160 | unieqi 4445 |
. 2
Poly
deg coeff |
162 | 158, 161 | eqtr4i 2647 |
1
|