Step | Hyp | Ref
| Expression |
1 | | elaa2lem.f |
. . . 4
deg |
2 | 1 | a1i 11 |
. . 3
deg |
3 | | zsscn 11385 |
. . . . 5
|
4 | 3 | a1i 11 |
. . . 4
|
5 | | elaa2lem.g |
. . . . . . . . 9
Poly |
6 | | dgrcl 23989 |
. . . . . . . . 9
Poly deg |
7 | 5, 6 | syl 17 |
. . . . . . . 8
deg |
8 | 7 | nn0zd 11480 |
. . . . . . 7
deg |
9 | | elaa2lem.m |
. . . . . . . . 9
inf
coeff |
10 | | ssrab2 3687 |
. . . . . . . . . 10
coeff |
11 | | nn0uz 11722 |
. . . . . . . . . . . . 13
|
12 | 10, 11 | sseqtri 3637 |
. . . . . . . . . . . 12
coeff |
13 | 12 | a1i 11 |
. . . . . . . . . . 11
coeff |
14 | | elaa2lem.gn0 |
. . . . . . . . . . . . . . . . 17
|
15 | 14 | neneqd 2799 |
. . . . . . . . . . . . . . . 16
|
16 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
deg deg |
17 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
coeff coeff |
18 | 16, 17 | dgreq0 24021 |
. . . . . . . . . . . . . . . . 17
Poly
coeffdeg |
19 | 5, 18 | syl 17 |
. . . . . . . . . . . . . . . 16
coeffdeg |
20 | 15, 19 | mtbid 314 |
. . . . . . . . . . . . . . 15
coeffdeg |
21 | 20 | neqned 2801 |
. . . . . . . . . . . . . 14
coeffdeg |
22 | 7, 21 | jca 554 |
. . . . . . . . . . . . 13
deg coeffdeg |
23 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
deg
coeff coeffdeg |
24 | 23 | neeq1d 2853 |
. . . . . . . . . . . . . 14
deg
coeff coeffdeg |
25 | 24 | elrab 3363 |
. . . . . . . . . . . . 13
deg coeff
deg coeffdeg |
26 | 22, 25 | sylibr 224 |
. . . . . . . . . . . 12
deg coeff |
27 | | ne0i 3921 |
. . . . . . . . . . . 12
deg coeff coeff |
28 | 26, 27 | syl 17 |
. . . . . . . . . . 11
coeff |
29 | | infssuzcl 11772 |
. . . . . . . . . . 11
coeff coeff inf coeff coeff |
30 | 13, 28, 29 | syl2anc 693 |
. . . . . . . . . 10
inf
coeff
coeff |
31 | 10, 30 | sseldi 3601 |
. . . . . . . . 9
inf
coeff |
32 | 9, 31 | syl5eqel 2705 |
. . . . . . . 8
|
33 | 32 | nn0zd 11480 |
. . . . . . 7
|
34 | 8, 33 | zsubcld 11487 |
. . . . . 6
deg |
35 | 9 | a1i 11 |
. . . . . . . 8
inf coeff |
36 | | infssuzle 11771 |
. . . . . . . . 9
coeff deg coeff inf coeff deg |
37 | 13, 26, 36 | syl2anc 693 |
. . . . . . . 8
inf
coeff deg |
38 | 35, 37 | eqbrtrd 4675 |
. . . . . . 7
deg |
39 | 7 | nn0red 11352 |
. . . . . . . 8
deg |
40 | 32 | nn0red 11352 |
. . . . . . . 8
|
41 | 39, 40 | subge0d 10617 |
. . . . . . 7
deg
deg |
42 | 38, 41 | mpbird 247 |
. . . . . 6
deg |
43 | 34, 42 | jca 554 |
. . . . 5
deg deg |
44 | | elnn0z 11390 |
. . . . 5
deg deg deg |
45 | 43, 44 | sylibr 224 |
. . . 4
deg |
46 | | id 22 |
. . . . . . . . 9
Poly Poly |
47 | | 0zd 11389 |
. . . . . . . . 9
Poly |
48 | 17 | coef2 23987 |
. . . . . . . . 9
Poly
coeff |
49 | 46, 47, 48 | syl2anc 693 |
. . . . . . . 8
Poly coeff |
50 | 5, 49 | syl 17 |
. . . . . . 7
coeff |
51 | 50 | adantr 481 |
. . . . . 6
coeff |
52 | | simpr 477 |
. . . . . . 7
|
53 | 32 | adantr 481 |
. . . . . . 7
|
54 | 52, 53 | nn0addcld 11355 |
. . . . . 6
|
55 | 51, 54 | ffvelrnd 6360 |
. . . . 5
coeff |
56 | | elaa2lem.i |
. . . . 5
coeff |
57 | 55, 56 | fmptd 6385 |
. . . 4
|
58 | | elplyr 23957 |
. . . 4
deg deg Poly |
59 | 4, 45, 57, 58 | syl3anc 1326 |
. . 3
deg Poly |
60 | 2, 59 | eqeltrd 2701 |
. 2
Poly |
61 | | simpr 477 |
. . . . . . . . . 10
deg
deg |
62 | 61 | iftrued 4094 |
. . . . . . . . 9
deg
deg coeff coeff |
63 | | iffalse 4095 |
. . . . . . . . . . 11
deg
deg coeff |
64 | 63 | adantl 482 |
. . . . . . . . . 10
deg deg coeff |
65 | | simpr 477 |
. . . . . . . . . . . . . . 15
deg deg |
66 | 39 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
deg deg |
67 | 40 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
deg |
68 | 66, 67 | resubcld 10458 |
. . . . . . . . . . . . . . . 16
deg deg |
69 | | nn0re 11301 |
. . . . . . . . . . . . . . . . 17
|
70 | 69 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
deg |
71 | 68, 70 | ltnled 10184 |
. . . . . . . . . . . . . . 15
deg deg
deg |
72 | 65, 71 | mpbird 247 |
. . . . . . . . . . . . . 14
deg deg |
73 | 66, 67, 70 | ltsubaddd 10623 |
. . . . . . . . . . . . . 14
deg deg
deg
|
74 | 72, 73 | mpbid 222 |
. . . . . . . . . . . . 13
deg deg |
75 | | olc 399 |
. . . . . . . . . . . . 13
deg
deg |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . 12
deg
deg |
77 | 5 | ad2antrr 762 |
. . . . . . . . . . . . 13
deg Poly |
78 | 54 | adantr 481 |
. . . . . . . . . . . . 13
deg |
79 | 16, 17 | dgrlt 24022 |
. . . . . . . . . . . . 13
Poly
deg deg coeff |
80 | 77, 78, 79 | syl2anc 693 |
. . . . . . . . . . . 12
deg deg deg coeff |
81 | 76, 80 | mpbid 222 |
. . . . . . . . . . 11
deg deg
coeff |
82 | 81 | simprd 479 |
. . . . . . . . . 10
deg coeff |
83 | 64, 82 | eqtr4d 2659 |
. . . . . . . . 9
deg deg coeff coeff |
84 | 62, 83 | pm2.61dan 832 |
. . . . . . . 8
deg coeff coeff |
85 | 84 | mpteq2dva 4744 |
. . . . . . 7
deg coeff coeff |
86 | 50, 4 | fssd 6057 |
. . . . . . . . . 10
coeff |
87 | 86 | adantr 481 |
. . . . . . . . 9
deg coeff |
88 | | elfznn0 12433 |
. . . . . . . . . . 11
deg
|
89 | 88 | adantl 482 |
. . . . . . . . . 10
deg |
90 | 32 | adantr 481 |
. . . . . . . . . 10
deg |
91 | 89, 90 | nn0addcld 11355 |
. . . . . . . . 9
deg |
92 | 87, 91 | ffvelrnd 6360 |
. . . . . . . 8
deg coeff |
93 | | eqidd 2623 |
. . . . . . . . . . 11
deg deg |
94 | | simpl 473 |
. . . . . . . . . . . . . 14
deg |
95 | 56 | a1i 11 |
. . . . . . . . . . . . . . 15
coeff |
96 | 95, 55 | fvmpt2d 6293 |
. . . . . . . . . . . . . 14
coeff |
97 | 94, 89, 96 | syl2anc 693 |
. . . . . . . . . . . . 13
deg coeff |
98 | 97 | adantlr 751 |
. . . . . . . . . . . 12
deg coeff |
99 | 98 | oveq1d 6665 |
. . . . . . . . . . 11
deg coeff |
100 | 93, 99 | sumeq12rdv 14438 |
. . . . . . . . . 10
deg deg coeff |
101 | 100 | mpteq2dva 4744 |
. . . . . . . . 9
deg deg coeff |
102 | 2, 101 | eqtrd 2656 |
. . . . . . . 8
deg coeff |
103 | 60, 45, 92, 102 | coeeq2 23998 |
. . . . . . 7
coeff deg coeff |
104 | 85, 103, 95 | 3eqtr4d 2666 |
. . . . . 6
coeff |
105 | 104 | fveq1d 6193 |
. . . . 5
coeff |
106 | | oveq1 6657 |
. . . . . . . . 9
|
107 | 106 | adantl 482 |
. . . . . . . 8
|
108 | 3, 33 | sseldi 3601 |
. . . . . . . . . 10
|
109 | 108 | addid2d 10237 |
. . . . . . . . 9
|
110 | 109 | adantr 481 |
. . . . . . . 8
|
111 | 107, 110 | eqtrd 2656 |
. . . . . . 7
|
112 | 111 | fveq2d 6195 |
. . . . . 6
coeff coeff |
113 | | 0nn0 11307 |
. . . . . . 7
|
114 | 113 | a1i 11 |
. . . . . 6
|
115 | 50, 32 | ffvelrnd 6360 |
. . . . . 6
coeff |
116 | 95, 112, 114, 115 | fvmptd 6288 |
. . . . 5
coeff |
117 | | eqidd 2623 |
. . . . 5
coeff coeff |
118 | 105, 116,
117 | 3eqtrd 2660 |
. . . 4
coeff coeff |
119 | 35, 30 | eqeltrd 2701 |
. . . . . 6
coeff |
120 | | fveq2 6191 |
. . . . . . . 8
coeff coeff |
121 | 120 | neeq1d 2853 |
. . . . . . 7
coeff
coeff |
122 | 121 | elrab 3363 |
. . . . . 6
coeff coeff |
123 | 119, 122 | sylib 208 |
. . . . 5
coeff |
124 | 123 | simprd 479 |
. . . 4
coeff |
125 | 118, 124 | eqnetrd 2861 |
. . 3
coeff |
126 | 5, 47 | syl 17 |
. . . . . . 7
|
127 | | aasscn 24073 |
. . . . . . . . . . 11
|
128 | | elaa2lem.a |
. . . . . . . . . . 11
|
129 | 127, 128 | sseldi 3601 |
. . . . . . . . . 10
|
130 | 94, 129 | syl 17 |
. . . . . . . . 9
deg |
131 | 130, 89 | expcld 13008 |
. . . . . . . 8
deg |
132 | 92, 131 | mulcld 10060 |
. . . . . . 7
deg coeff |
133 | | oveq1 6657 |
. . . . . . . . 9
|
134 | 133 | fveq2d 6195 |
. . . . . . . 8
coeff coeff |
135 | | oveq2 6658 |
. . . . . . . 8
|
136 | 134, 135 | oveq12d 6668 |
. . . . . . 7
coeff coeff |
137 | 33, 126, 34, 132, 136 | fsumshft 14512 |
. . . . . 6
deg coeff
deg coeff |
138 | 3, 8 | sseldi 3601 |
. . . . . . . . . 10
deg |
139 | 138, 108 | npcand 10396 |
. . . . . . . . 9
deg deg |
140 | 109, 139 | oveq12d 6668 |
. . . . . . . 8
deg deg |
141 | 140 | sumeq1d 14431 |
. . . . . . 7
deg coeff degcoeff |
142 | | elfzelz 12342 |
. . . . . . . . . . . . . 14
deg |
143 | 142 | adantl 482 |
. . . . . . . . . . . . 13
deg |
144 | 3, 143 | sseldi 3601 |
. . . . . . . . . . . 12
deg |
145 | 108 | adantr 481 |
. . . . . . . . . . . 12
deg |
146 | 144, 145 | npcand 10396 |
. . . . . . . . . . 11
deg |
147 | 146 | fveq2d 6195 |
. . . . . . . . . 10
deg coeff coeff |
148 | 147 | oveq1d 6665 |
. . . . . . . . 9
deg coeff coeff |
149 | 129 | adantr 481 |
. . . . . . . . . . . 12
deg |
150 | | elaa2lem.an0 |
. . . . . . . . . . . . 13
|
151 | 150 | adantr 481 |
. . . . . . . . . . . 12
deg |
152 | 33 | adantr 481 |
. . . . . . . . . . . 12
deg |
153 | 149, 151,
152, 143 | expsubd 13019 |
. . . . . . . . . . 11
deg |
154 | 153 | oveq2d 6666 |
. . . . . . . . . 10
deg coeff coeff |
155 | 86 | adantr 481 |
. . . . . . . . . . . . 13
deg coeff |
156 | | 0red 10041 |
. . . . . . . . . . . . . . . 16
deg |
157 | 40 | adantr 481 |
. . . . . . . . . . . . . . . 16
deg |
158 | 143 | zred 11482 |
. . . . . . . . . . . . . . . 16
deg |
159 | 32 | nn0ge0d 11354 |
. . . . . . . . . . . . . . . . 17
|
160 | 159 | adantr 481 |
. . . . . . . . . . . . . . . 16
deg |
161 | | elfzle1 12344 |
. . . . . . . . . . . . . . . . 17
deg |
162 | 161 | adantl 482 |
. . . . . . . . . . . . . . . 16
deg |
163 | 156, 157,
158, 160, 162 | letrd 10194 |
. . . . . . . . . . . . . . 15
deg |
164 | 143, 163 | jca 554 |
. . . . . . . . . . . . . 14
deg |
165 | | elnn0z 11390 |
. . . . . . . . . . . . . 14
|
166 | 164, 165 | sylibr 224 |
. . . . . . . . . . . . 13
deg |
167 | 155, 166 | ffvelrnd 6360 |
. . . . . . . . . . . 12
deg coeff |
168 | 149, 166 | expcld 13008 |
. . . . . . . . . . . 12
deg |
169 | 129, 32 | expcld 13008 |
. . . . . . . . . . . . 13
|
170 | 169 | adantr 481 |
. . . . . . . . . . . 12
deg |
171 | 149, 151,
152 | expne0d 13014 |
. . . . . . . . . . . 12
deg |
172 | 167, 168,
170, 171 | divassd 10836 |
. . . . . . . . . . 11
deg coeff coeff |
173 | 172 | eqcomd 2628 |
. . . . . . . . . 10
deg coeff coeff |
174 | 154, 173 | eqtr2d 2657 |
. . . . . . . . 9
deg coeff coeff |
175 | 148, 174 | eqtr4d 2659 |
. . . . . . . 8
deg coeff coeff |
176 | 175 | sumeq2dv 14433 |
. . . . . . 7
degcoeff degcoeff |
177 | 141, 176 | eqtrd 2656 |
. . . . . 6
deg coeff degcoeff |
178 | 32, 11 | syl6eleq 2711 |
. . . . . . . 8
|
179 | | fzss1 12380 |
. . . . . . . 8
deg
deg |
180 | 178, 179 | syl 17 |
. . . . . . 7
deg deg |
181 | 167, 168 | mulcld 10060 |
. . . . . . . 8
deg coeff |
182 | 181, 170,
171 | divcld 10801 |
. . . . . . 7
deg coeff |
183 | 33 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
deg
deg
|
184 | 8 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
deg
deg
deg |
185 | | eldifi 3732 |
. . . . . . . . . . . . . . . . . . 19
deg deg deg |
186 | | elfznn0 12433 |
. . . . . . . . . . . . . . . . . . . 20
deg
|
187 | 186 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . 19
deg
|
188 | 185, 187 | syl 17 |
. . . . . . . . . . . . . . . . . 18
deg deg |
189 | 188 | ad2antlr 763 |
. . . . . . . . . . . . . . . . 17
deg
deg
|
190 | 183, 184,
189 | 3jca 1242 |
. . . . . . . . . . . . . . . 16
deg
deg
deg |
191 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
deg
deg
|
192 | 40 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
deg
deg
|
193 | 189 | zred 11482 |
. . . . . . . . . . . . . . . . . 18
deg
deg
|
194 | 192, 193 | lenltd 10183 |
. . . . . . . . . . . . . . . . 17
deg
deg
|
195 | 191, 194 | mpbird 247 |
. . . . . . . . . . . . . . . 16
deg
deg
|
196 | | elfzle2 12345 |
. . . . . . . . . . . . . . . . . 18
deg
deg |
197 | 185, 196 | syl 17 |
. . . . . . . . . . . . . . . . 17
deg deg
deg |
198 | 197 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
deg
deg
deg |
199 | 190, 195,
198 | jca32 558 |
. . . . . . . . . . . . . . 15
deg
deg
deg
deg |
200 | | elfz2 12333 |
. . . . . . . . . . . . . . 15
deg deg
deg |
201 | 199, 200 | sylibr 224 |
. . . . . . . . . . . . . 14
deg
deg
deg |
202 | | eldifn 3733 |
. . . . . . . . . . . . . . 15
deg deg
deg |
203 | 202 | ad2antlr 763 |
. . . . . . . . . . . . . 14
deg
deg
deg |
204 | 201, 203 | condan 835 |
. . . . . . . . . . . . 13
deg
deg
|
205 | 204 | adantr 481 |
. . . . . . . . . . . 12
deg
deg coeff
|
206 | 9 | a1i 11 |
. . . . . . . . . . . . . 14
deg
deg coeff
inf coeff |
207 | 12 | a1i 11 |
. . . . . . . . . . . . . . 15
deg
deg coeff
coeff |
208 | 185, 186 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
deg deg |
209 | 208 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
deg deg coeff |
210 | | neqne 2802 |
. . . . . . . . . . . . . . . . . . 19
coeff coeff |
211 | 210 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
deg deg coeff coeff |
212 | 209, 211 | jca 554 |
. . . . . . . . . . . . . . . . 17
deg deg coeff
coeff |
213 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
coeff coeff |
214 | 213 | neeq1d 2853 |
. . . . . . . . . . . . . . . . . 18
coeff
coeff |
215 | 214 | elrab 3363 |
. . . . . . . . . . . . . . . . 17
coeff coeff |
216 | 212, 215 | sylibr 224 |
. . . . . . . . . . . . . . . 16
deg deg coeff coeff |
217 | 216 | adantll 750 |
. . . . . . . . . . . . . . 15
deg
deg coeff coeff |
218 | | infssuzle 11771 |
. . . . . . . . . . . . . . 15
coeff
coeff
inf coeff |
219 | 207, 217,
218 | syl2anc 693 |
. . . . . . . . . . . . . 14
deg
deg coeff inf coeff |
220 | 206, 219 | eqbrtrd 4675 |
. . . . . . . . . . . . 13
deg
deg coeff |
221 | 40 | ad2antrr 762 |
. . . . . . . . . . . . . 14
deg
deg coeff
|
222 | 188 | zred 11482 |
. . . . . . . . . . . . . . 15
deg deg |
223 | 222 | ad2antlr 763 |
. . . . . . . . . . . . . 14
deg
deg coeff |
224 | 221, 223 | lenltd 10183 |
. . . . . . . . . . . . 13
deg
deg coeff |
225 | 220, 224 | mpbid 222 |
. . . . . . . . . . . 12
deg
deg coeff
|
226 | 205, 225 | condan 835 |
. . . . . . . . . . 11
deg
deg coeff |
227 | 226 | oveq1d 6665 |
. . . . . . . . . 10
deg
deg coeff |
228 | 129 | adantr 481 |
. . . . . . . . . . . 12
deg
deg
|
229 | 208 | adantl 482 |
. . . . . . . . . . . 12
deg
deg |
230 | 228, 229 | expcld 13008 |
. . . . . . . . . . 11
deg
deg |
231 | 230 | mul02d 10234 |
. . . . . . . . . 10
deg
deg |
232 | 227, 231 | eqtrd 2656 |
. . . . . . . . 9
deg
deg coeff |
233 | 232 | oveq1d 6665 |
. . . . . . . 8
deg
deg coeff |
234 | 129, 150,
33 | expne0d 13014 |
. . . . . . . . . 10
|
235 | 169, 234 | div0d 10800 |
. . . . . . . . 9
|
236 | 235 | adantr 481 |
. . . . . . . 8
deg
deg |
237 | 233, 236 | eqtrd 2656 |
. . . . . . 7
deg
deg coeff |
238 | | fzfid 12772 |
. . . . . . 7
deg |
239 | 180, 182,
237, 238 | fsumss 14456 |
. . . . . 6
degcoeff degcoeff |
240 | 137, 177,
239 | 3eqtrd 2660 |
. . . . 5
deg coeff
degcoeff |
241 | 89, 55 | syldan 487 |
. . . . . . . . . 10
deg coeff |
242 | 56 | fvmpt2 6291 |
. . . . . . . . . 10
coeff coeff |
243 | 89, 241, 242 | syl2anc 693 |
. . . . . . . . 9
deg coeff |
244 | 243 | adantlr 751 |
. . . . . . . 8
deg coeff |
245 | | oveq1 6657 |
. . . . . . . . 9
|
246 | 245 | ad2antlr 763 |
. . . . . . . 8
deg |
247 | 244, 246 | oveq12d 6668 |
. . . . . . 7
deg coeff |
248 | 247 | sumeq2dv 14433 |
. . . . . 6
deg deg coeff |
249 | | fzfid 12772 |
. . . . . . 7
deg |
250 | 249, 132 | fsumcl 14464 |
. . . . . 6
deg coeff |
251 | 2, 248, 129, 250 | fvmptd 6288 |
. . . . 5
deg coeff |
252 | 17, 16 | coeid2 23995 |
. . . . . . . 8
Poly
degcoeff |
253 | 5, 129, 252 | syl2anc 693 |
. . . . . . 7
degcoeff |
254 | 253 | oveq1d 6665 |
. . . . . 6
degcoeff |
255 | 86 | adantr 481 |
. . . . . . . . 9
deg coeff |
256 | 186 | adantl 482 |
. . . . . . . . 9
deg |
257 | 255, 256 | ffvelrnd 6360 |
. . . . . . . 8
deg coeff |
258 | 129 | adantr 481 |
. . . . . . . . 9
deg |
259 | 258, 256 | expcld 13008 |
. . . . . . . 8
deg |
260 | 257, 259 | mulcld 10060 |
. . . . . . 7
deg coeff |
261 | 238, 169,
260, 234 | fsumdivc 14518 |
. . . . . 6
degcoeff degcoeff |
262 | 254, 261 | eqtrd 2656 |
. . . . 5
degcoeff |
263 | 240, 251,
262 | 3eqtr4d 2666 |
. . . 4
|
264 | | elaa2lem.ga |
. . . . 5
|
265 | 264 | oveq1d 6665 |
. . . 4
|
266 | 263, 265,
235 | 3eqtrd 2660 |
. . 3
|
267 | 125, 266 | jca 554 |
. 2
coeff |
268 | | fveq2 6191 |
. . . . . 6
coeff coeff |
269 | 268 | fveq1d 6193 |
. . . . 5
coeff coeff |
270 | 269 | neeq1d 2853 |
. . . 4
coeff
coeff |
271 | | fveq1 6190 |
. . . . 5
|
272 | 271 | eqeq1d 2624 |
. . . 4
|
273 | 270, 272 | anbi12d 747 |
. . 3
coeff coeff |
274 | 273 | rspcev 3309 |
. 2
Poly
coeff
Polycoeff |
275 | 60, 267, 274 | syl2anc 693 |
1
Polycoeff |