Step | Hyp | Ref
| Expression |
1 | | vieta1.5 |
. . . . 5
       |
2 | | vieta1lem.7 |
. . . . . . 7
     |
3 | | vieta1lem.6 |
. . . . . . . 8
   |
4 | 3 | peano2nnd 10648 |
. . . . . . 7
     |
5 | 2, 4 | eqeltrrd 2550 |
. . . . . 6
   |
6 | 5 | nnne0d 10676 |
. . . . 5
   |
7 | 1, 6 | eqnetrd 2710 |
. . . 4
       |
8 | | vieta1.4 |
. . . . . . . 8
 Poly    |
9 | | vieta1.2 |
. . . . . . . . . 10
deg   |
10 | 9, 6 | syl5eqner 2718 |
. . . . . . . . 9
 deg    |
11 | | fveq2 5879 |
. . . . . . . . . . 11
  deg  deg     |
12 | | dgr0 23295 |
. . . . . . . . . . 11
deg    |
13 | 11, 12 | syl6eq 2521 |
. . . . . . . . . 10
  deg    |
14 | 13 | necon3i 2675 |
. . . . . . . . 9
 deg 
   |
15 | 10, 14 | syl 17 |
. . . . . . . 8
    |
16 | | vieta1.3 |
. . . . . . . . 9
        |
17 | 16 | fta1 23340 |
. . . . . . . 8
  Poly        
deg     |
18 | 8, 15, 17 | syl2anc 673 |
. . . . . . 7
     
deg     |
19 | 18 | simpld 466 |
. . . . . 6
   |
20 | | hasheq0 12582 |
. . . . . 6
     
   |
21 | 19, 20 | syl 17 |
. . . . 5
         |
22 | 21 | necon3bid 2687 |
. . . 4
         |
23 | 7, 22 | mpbid 215 |
. . 3
   |
24 | | n0 3732 |
. . 3
    |
25 | 23, 24 | sylib 201 |
. 2
    |
26 | | incom 3616 |
. . . . 5
                       |
27 | | vieta1.1 |
. . . . . . . . . . 11
coeff   |
28 | | vieta1lem.8 |
. . . . . . . . . . 11
  Poly     deg             deg               coeff     deg     coeff    deg       |
29 | | vieta1lem.9 |
. . . . . . . . . . 11
 quot    
      |
30 | 27, 9, 16, 8, 1, 3,
2, 28, 29 | vieta1lem1 23342 |
. . . . . . . . . 10
 
 
Poly  deg     |
31 | 30 | simprd 470 |
. . . . . . . . 9
 
 deg    |
32 | 30 | simpld 466 |
. . . . . . . . . . 11
 
 Poly    |
33 | | dgrcl 23266 |
. . . . . . . . . . 11
 Poly  deg    |
34 | 32, 33 | syl 17 |
. . . . . . . . . 10
 
 deg    |
35 | 34 | nn0red 10950 |
. . . . . . . . 9
 
 deg    |
36 | 31, 35 | eqeltrd 2549 |
. . . . . . . 8
 
   |
37 | 36 | ltp1d 10559 |
. . . . . . . 8
 
     |
38 | 36, 37 | gtned 9787 |
. . . . . . 7
 
 
   |
39 | | snssi 4107 |
. . . . . . . . . . 11
                   |
40 | | ssequn1 3595 |
. . . . . . . . . . 11
         
                    |
41 | 39, 40 | sylib 201 |
. . . . . . . . . 10
                            |
42 | 41 | fveq2d 5883 |
. . . . . . . . 9
                                    |
43 | 8 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
 
 Poly    |
44 | | cnvimass 5194 |
. . . . . . . . . . . . . . . . . . . . 21
        |
45 | 16, 44 | eqsstri 3448 |
. . . . . . . . . . . . . . . . . . . 20
 |
46 | | plyf 23231 |
. . . . . . . . . . . . . . . . . . . . 21
 Poly 
      |
47 | | fdm 5745 |
. . . . . . . . . . . . . . . . . . . . 21
       |
48 | 8, 46, 47 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
   |
49 | 45, 48 | syl5sseq 3466 |
. . . . . . . . . . . . . . . . . . 19

  |
50 | 49 | sselda 3418 |
. . . . . . . . . . . . . . . . . 18
 
   |
51 | 16 | eleq2i 2541 |
. . . . . . . . . . . . . . . . . . . 20

         |
52 | | ffn 5739 |
. . . . . . . . . . . . . . . . . . . . 21
       |
53 | | fniniseg 6018 |
. . . . . . . . . . . . . . . . . . . . 21
        
         |
54 | 8, 46, 52, 53 | 4syl 19 |
. . . . . . . . . . . . . . . . . . . 20
        
         |
55 | 51, 54 | syl5bb 265 |
. . . . . . . . . . . . . . . . . . 19
           |
56 | 55 | simplbda 636 |
. . . . . . . . . . . . . . . . . 18
 
       |
57 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . 19
   
             |
58 | 57 | facth 23338 |
. . . . . . . . . . . . . . . . . 18
  Poly           
      quot             |
59 | 43, 50, 56, 58 | syl3anc 1292 |
. . . . . . . . . . . . . . . . 17
 
     
      quot             |
60 | 29 | oveq2i 6319 |
. . . . . . . . . . . . . . . . 17
                      quot            |
61 | 59, 60 | syl6eqr 2523 |
. . . . . . . . . . . . . . . 16
 
     
        |
62 | 61 | cnveqd 5015 |
. . . . . . . . . . . . . . 15
 
 
              |
63 | 62 | imaeq1d 5173 |
. . . . . . . . . . . . . 14
 
              
             |
64 | 16, 63 | syl5eq 2517 |
. . . . . . . . . . . . 13
 
                     |
65 | | cnex 9638 |
. . . . . . . . . . . . . . 15
 |
66 | 65 | a1i 11 |
. . . . . . . . . . . . . 14
 
   |
67 | 57 | plyremlem 23336 |
. . . . . . . . . . . . . . . . 17
          Poly  deg                              |
68 | 50, 67 | syl 17 |
. . . . . . . . . . . . . . . 16
 
          Poly  deg                              |
69 | 68 | simp1d 1042 |
. . . . . . . . . . . . . . 15
 
         Poly    |
70 | | plyf 23231 |
. . . . . . . . . . . . . . 15
         Poly 
   
          |
71 | 69, 70 | syl 17 |
. . . . . . . . . . . . . 14
 
               |
72 | | plyf 23231 |
. . . . . . . . . . . . . . 15
 Poly        |
73 | 32, 72 | syl 17 |
. . . . . . . . . . . . . 14
 
       |
74 | | ofmulrt 23314 |
. . . . . . . . . . . . . 14
                  
                                            |
75 | 66, 71, 73, 74 | syl3anc 1292 |
. . . . . . . . . . . . 13
 
       
                                     |
76 | 68 | simp3d 1044 |
. . . . . . . . . . . . . 14
 
                    |
77 | 76 | uneq1d 3578 |
. . . . . . . . . . . . 13
 
       
                              |
78 | 64, 75, 77 | 3eqtrd 2509 |
. . . . . . . . . . . 12
 
              |
79 | 78 | fveq2d 5883 |
. . . . . . . . . . 11
 
                      |
80 | 1, 2 | eqtr4d 2508 |
. . . . . . . . . . . 12
         |
81 | 80 | adantr 472 |
. . . . . . . . . . 11
 
         |
82 | 79, 81 | eqtr3d 2507 |
. . . . . . . . . 10
 
                    |
83 | 15 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
 
    |
84 | 61, 83 | eqnetrrd 2711 |
. . . . . . . . . . . . . . . . 17
 
               |
85 | | plymul0or 23313 |
. . . . . . . . . . . . . . . . . . 19
          Poly  Poly  
            
               |
86 | 69, 32, 85 | syl2anc 673 |
. . . . . . . . . . . . . . . . . 18
 
             
               |
87 | 86 | necon3abid 2679 |
. . . . . . . . . . . . . . . . 17
 
             
               |
88 | 84, 87 | mpbid 215 |
. . . . . . . . . . . . . . . 16
 
               |
89 | | neanior 2735 |
. . . . . . . . . . . . . . . 16
            
              |
90 | 88, 89 | sylibr 217 |
. . . . . . . . . . . . . . 15
 
               |
91 | 90 | simprd 470 |
. . . . . . . . . . . . . 14
 
    |
92 | | eqid 2471 |
. . . . . . . . . . . . . . 15
               |
93 | 92 | fta1 23340 |
. . . . . . . . . . . . . 14
  Poly 
                    
deg     |
94 | 32, 91, 93 | syl2anc 673 |
. . . . . . . . . . . . 13
 
                   
deg     |
95 | 94 | simprd 470 |
. . . . . . . . . . . 12
 
           
deg    |
96 | 95, 31 | breqtrrd 4422 |
. . . . . . . . . . 11
 
           
  |
97 | | snfi 7668 |
. . . . . . . . . . . . . 14
   |
98 | 94 | simpld 466 |
. . . . . . . . . . . . . 14
 
          |
99 | | hashun2 12600 |
. . . . . . . . . . . . . 14
                                                |
100 | 97, 98, 99 | sylancr 676 |
. . . . . . . . . . . . 13
 
                                     |
101 | | ax-1cn 9615 |
. . . . . . . . . . . . . . 15
 |
102 | 3 | nncnd 10647 |
. . . . . . . . . . . . . . . 16
   |
103 | 102 | adantr 472 |
. . . . . . . . . . . . . . 15
 
   |
104 | | addcom 9837 |
. . . . . . . . . . . . . . 15
 
       |
105 | 101, 103,
104 | sylancr 676 |
. . . . . . . . . . . . . 14
 
       |
106 | 82, 105 | eqtr4d 2508 |
. . . . . . . . . . . . 13
 
                    |
107 | | hashsng 12587 |
. . . . . . . . . . . . . . 15
         |
108 | 107 | adantl 473 |
. . . . . . . . . . . . . 14
 
         |
109 | 108 | oveq1d 6323 |
. . . . . . . . . . . . 13
 
                                   |
110 | 100, 106,
109 | 3brtr3d 4425 |
. . . . . . . . . . . 12
 
                  |
111 | | hashcl 12576 |
. . . . . . . . . . . . . . 15
                     |
112 | 98, 111 | syl 17 |
. . . . . . . . . . . . . 14
 
              |
113 | 112 | nn0red 10950 |
. . . . . . . . . . . . 13
 
              |
114 | | 1red 9676 |
. . . . . . . . . . . . 13
 
   |
115 | 36, 113, 114 | leadd2d 10229 |
. . . . . . . . . . . 12
 
            
                  |
116 | 110, 115 | mpbird 240 |
. . . . . . . . . . 11
 
              |
117 | 113, 36 | letri3d 9794 |
. . . . . . . . . . 11
 
                        
               |
118 | 96, 116, 117 | mpbir2and 936 |
. . . . . . . . . 10
 
              |
119 | 82, 118 | eqeq12d 2486 |
. . . . . . . . 9
 
                           
     |
120 | 42, 119 | syl5ib 227 |
. . . . . . . 8
 
         
    |
121 | 120 | necon3ad 2656 |
. . . . . . 7
 
   
          |
122 | 38, 121 | mpd 15 |
. . . . . 6
 

         |
123 | | disjsn 4023 |
. . . . . 6
           
         |
124 | 122, 123 | sylibr 217 |
. . . . 5
 
              |
125 | 26, 124 | syl5eq 2517 |
. . . 4
 
              |
126 | 19 | adantr 472 |
. . . 4
 
   |
127 | 49 | adantr 472 |
. . . . 5
 
   |
128 | 127 | sselda 3418 |
. . . 4
       |
129 | 125, 78, 126, 128 | fsumsplit 13883 |
. . 3
 
 
                 |
130 | | id 22 |
. . . . . . 7
   |
131 | 130 | sumsn 13884 |
. . . . . 6
 
 
     |
132 | 50, 50, 131 | syl2anc 673 |
. . . . 5
 
       |
133 | 50 | negnegd 9996 |
. . . . 5
 
     |
134 | 132, 133 | eqtr4d 2508 |
. . . 4
 
         |
135 | 118, 31 | eqtrd 2505 |
. . . . . 6
 
            deg    |
136 | 28 | adantr 472 |
. . . . . . 7
 
  Poly     deg             deg               coeff     deg     coeff    deg       |
137 | | fveq2 5879 |
. . . . . . . . . . 11
 deg  deg    |
138 | 137 | eqeq2d 2481 |
. . . . . . . . . 10
 
deg 
deg     |
139 | | cnveq 5013 |
. . . . . . . . . . . . 13
 
   |
140 | 139 | imaeq1d 5173 |
. . . . . . . . . . . 12
                 |
141 | 140 | fveq2d 5883 |
. . . . . . . . . . 11
                         |
142 | 141, 137 | eqeq12d 2486 |
. . . . . . . . . 10
             deg             deg     |
143 | 138, 142 | anbi12d 725 |
. . . . . . . . 9
   deg             deg    deg             deg      |
144 | 140 | sumeq1d 13844 |
. . . . . . . . . 10
                     |
145 | | fveq2 5879 |
. . . . . . . . . . . . 13
 coeff  coeff    |
146 | 137 | oveq1d 6323 |
. . . . . . . . . . . . 13
  deg    deg     |
147 | 145, 146 | fveq12d 5885 |
. . . . . . . . . . . 12
  coeff     deg     coeff     deg      |
148 | 145, 137 | fveq12d 5885 |
. . . . . . . . . . . 12
  coeff    deg    coeff    deg     |
149 | 147, 148 | oveq12d 6326 |
. . . . . . . . . . 11
   coeff     deg     coeff    deg      coeff     deg     coeff    deg      |
150 | 149 | negeqd 9889 |
. . . . . . . . . 10
    coeff     deg     coeff    deg       coeff     deg     coeff    deg      |
151 | 144, 150 | eqeq12d 2486 |
. . . . . . . . 9
              coeff     deg     coeff    deg                coeff     deg     coeff    deg       |
152 | 143, 151 | imbi12d 327 |
. . . . . . . 8
    deg             deg               coeff     deg     coeff    deg    
 
deg 
           deg  
            coeff     deg     coeff    deg        |
153 | 152 | rspcv 3132 |
. . . . . . 7
 Poly    Poly     deg             deg               coeff     deg     coeff    deg       deg             deg  
            coeff     deg     coeff    deg        |
154 | 32, 136, 153 | sylc 61 |
. . . . . 6
 
   deg             deg  
            coeff     deg     coeff    deg       |
155 | 31, 135, 154 | mp2and 693 |
. . . . 5
 
             coeff     deg     coeff    deg      |
156 | 31 | oveq1d 6323 |
. . . . . . . 8
 
 
  deg     |
157 | 156 | fveq2d 5883 |
. . . . . . 7
 
  coeff        coeff     deg      |
158 | 61 | fveq2d 5883 |
. . . . . . . . . 10
 
 coeff  coeff               |
159 | 27, 158 | syl5eq 2517 |
. . . . . . . . 9
 
 coeff               |
160 | 61 | fveq2d 5883 |
. . . . . . . . . . 11
 
 deg  deg     
         |
161 | 68 | simp2d 1043 |
. . . . . . . . . . . . . 14
 
 deg            |
162 | | ax-1ne0 9626 |
. . . . . . . . . . . . . . 15
 |
163 | 162 | a1i 11 |
. . . . . . . . . . . . . 14
 
   |
164 | 161, 163 | eqnetrd 2710 |
. . . . . . . . . . . . 13
 
 deg            |
165 | | fveq2 5879 |
. . . . . . . . . . . . . . 15
          deg          deg     |
166 | 165, 12 | syl6eq 2521 |
. . . . . . . . . . . . . 14
          deg            |
167 | 166 | necon3i 2675 |
. . . . . . . . . . . . 13
 deg         
           |
168 | 164, 167 | syl 17 |
. . . . . . . . . . . 12
 
            |
169 | | eqid 2471 |
. . . . . . . . . . . . 13
deg          deg           |
170 | | eqid 2471 |
. . . . . . . . . . . . 13
deg  deg   |
171 | 169, 170 | dgrmul 23303 |
. . . . . . . . . . . 12
           Poly             Poly     deg              deg          deg     |
172 | 69, 168, 32, 91, 171 | syl22anc 1293 |
. . . . . . . . . . 11
 
 deg              deg          deg     |
173 | 160, 172 | eqtrd 2505 |
. . . . . . . . . 10
 
 deg   deg          deg     |
174 | 9, 173 | syl5eq 2517 |
. . . . . . . . 9
 
  deg          deg     |
175 | 159, 174 | fveq12d 5885 |
. . . . . . . 8
 
      coeff                deg          deg      |
176 | | eqid 2471 |
. . . . . . . . . 10
coeff          coeff           |
177 | | eqid 2471 |
. . . . . . . . . 10
coeff  coeff   |
178 | 176, 177,
169, 170 | coemulhi 23287 |
. . . . . . . . 9
          Poly  Poly  
 coeff                deg          deg      coeff            deg            coeff    deg      |
179 | 69, 32, 178 | syl2anc 673 |
. . . . . . . 8
 
  coeff                deg          deg      coeff            deg            coeff    deg      |
180 | 161 | fveq2d 5883 |
. . . . . . . . . . 11
 
  coeff            deg            coeff               |
181 | | ssid 3437 |
. . . . . . . . . . . . . . 15
 |
182 | | plyid 23242 |
. . . . . . . . . . . . . . 15
 
 
Poly    |
183 | 181, 101,
182 | mp2an 686 |
. . . . . . . . . . . . . 14
 Poly   |
184 | | plyconst 23239 |
. . . . . . . . . . . . . . 15
 
     Poly    |
185 | 181, 50, 184 | sylancr 676 |
. . . . . . . . . . . . . 14
 
     Poly    |
186 | | eqid 2471 |
. . . . . . . . . . . . . . 15
coeff   coeff    |
187 | | eqid 2471 |
. . . . . . . . . . . . . . 15
coeff 
    coeff       |
188 | 186, 187 | coesub 23290 |
. . . . . . . . . . . . . 14
   Poly      Poly   coeff           coeff    coeff         |
189 | 183, 185,
188 | sylancr 676 |
. . . . . . . . . . . . 13
 
 coeff           coeff    coeff         |
190 | 189 | fveq1d 5881 |
. . . . . . . . . . . 12
 
  coeff               coeff    coeff            |
191 | | 1nn0 10909 |
. . . . . . . . . . . . . 14
 |
192 | 186 | coef3 23265 |
. . . . . . . . . . . . . . . . 17
  Poly 
coeff         |
193 | | ffn 5739 |
. . . . . . . . . . . . . . . . 17
 coeff       coeff     |
194 | 183, 192,
193 | mp2b 10 |
. . . . . . . . . . . . . . . 16
coeff    |
195 | 194 | a1i 11 |
. . . . . . . . . . . . . . 15
 
 coeff     |
196 | 187 | coef3 23265 |
. . . . . . . . . . . . . . . 16
     Poly  coeff            |
197 | | ffn 5739 |
. . . . . . . . . . . . . . . 16
 coeff          coeff        |
198 | 185, 196,
197 | 3syl 18 |
. . . . . . . . . . . . . . 15
 
 coeff        |
199 | | nn0ex 10899 |
. . . . . . . . . . . . . . . 16
 |
200 | 199 | a1i 11 |
. . . . . . . . . . . . . . 15
 
   |
201 | | inidm 3632 |
. . . . . . . . . . . . . . 15
   |
202 | | coeidp 23296 |
. . . . . . . . . . . . . . . . 17

 coeff             |
203 | 202 | adantl 473 |
. . . . . . . . . . . . . . . 16
      coeff             |
204 | | eqid 2471 |
. . . . . . . . . . . . . . . . 17
 |
205 | 204 | iftruei 3879 |
. . . . . . . . . . . . . . . 16
      |
206 | 203, 205 | syl6eq 2521 |
. . . . . . . . . . . . . . 15
      coeff        |
207 | | 0lt1 10157 |
. . . . . . . . . . . . . . . . . 18
 |
208 | | 0re 9661 |
. . . . . . . . . . . . . . . . . . 19
 |
209 | | 1re 9660 |
. . . . . . . . . . . . . . . . . . 19
 |
210 | 208, 209 | ltnlei 9773 |
. . . . . . . . . . . . . . . . . 18

  |
211 | 207, 210 | mpbi 213 |
. . . . . . . . . . . . . . . . 17
 |
212 | 50 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
       |
213 | | 0dgr 23278 |
. . . . . . . . . . . . . . . . . . 19
 deg        |
214 | 212, 213 | syl 17 |
. . . . . . . . . . . . . . . . . 18
     deg        |
215 | 214 | breq2d 4407 |
. . . . . . . . . . . . . . . . 17
     
deg     
   |
216 | 211, 215 | mtbiri 310 |
. . . . . . . . . . . . . . . 16
     deg        |
217 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . . 20
deg 
    deg       |
218 | 187, 217 | dgrub 23267 |
. . . . . . . . . . . . . . . . . . 19
      Poly 
 coeff          deg        |
219 | 218 | 3expia 1233 |
. . . . . . . . . . . . . . . . . 18
      Poly 
   coeff        
deg         |
220 | 185, 219 | sylan 479 |
. . . . . . . . . . . . . . . . 17
       coeff        
deg         |
221 | 220 | necon1bd 2661 |
. . . . . . . . . . . . . . . 16
     
deg 
     coeff            |
222 | 216, 221 | mpd 15 |
. . . . . . . . . . . . . . 15
      coeff           |
223 | 195, 198,
200, 200, 201, 206, 222 | ofval 6559 |
. . . . . . . . . . . . . 14
       coeff    coeff              |
224 | 191, 223 | mpan2 685 |
. . . . . . . . . . . . 13
 
   coeff    coeff              |
225 | | 1m0e1 10742 |
. . . . . . . . . . . . 13
   |
226 | 224, 225 | syl6eq 2521 |
. . . . . . . . . . . 12
 
   coeff    coeff            |
227 | 190, 226 | eqtrd 2505 |
. . . . . . . . . . 11
 
  coeff               |
228 | 180, 227 | eqtrd 2505 |
. . . . . . . . . 10
 
  coeff            deg             |
229 | 228 | oveq1d 6323 |
. . . . . . . . 9
 
   coeff            deg            coeff    deg      coeff    deg      |
230 | 177 | coef3 23265 |
. . . . . . . . . . . 12
 Poly  coeff        |
231 | 32, 230 | syl 17 |
. . . . . . . . . . 11
 
 coeff        |
232 | 231, 34 | ffvelrnd 6038 |
. . . . . . . . . 10
 
  coeff    deg     |
233 | 232 | mulid2d 9679 |
. . . . . . . . 9
 
   coeff    deg     coeff    deg     |
234 | 229, 233 | eqtrd 2505 |
. . . . . . . 8
 
   coeff            deg            coeff    deg     coeff    deg     |
235 | 175, 179,
234 | 3eqtrd 2509 |
. . . . . . 7
 
      coeff    deg     |
236 | 157, 235 | oveq12d 6326 |
. . . . . 6
 
   coeff              coeff     deg     coeff    deg      |
237 | 236 | negeqd 9889 |
. . . . 5
 
    coeff               coeff     deg     coeff    deg      |
238 | 155, 237 | eqtr4d 2508 |
. . . 4
 
             coeff              |
239 | 134, 238 | oveq12d 6326 |
. . 3
 
                      coeff    
          |
240 | 50 | negcld 9992 |
. . . . 5
 
    |
241 | | nnm1nn0 10935 |
. . . . . . . . 9
 
   |
242 | 3, 241 | syl 17 |
. . . . . . . 8
     |
243 | 242 | adantr 472 |
. . . . . . 7
 
 
   |
244 | 231, 243 | ffvelrnd 6038 |
. . . . . 6
 
  coeff         |
245 | 235, 232 | eqeltrd 2549 |
. . . . . 6
 
       |
246 | 9, 27 | dgreq0 23298 |
. . . . . . . . 9
 Poly 
 
       |
247 | 43, 246 | syl 17 |
. . . . . . . 8
 
 
        |
248 | 247 | necon3bid 2687 |
. . . . . . 7
 
  
       |
249 | 83, 248 | mpbid 215 |
. . . . . 6
 
       |
250 | 244, 245,
249 | divcld 10405 |
. . . . 5
 
   coeff              |
251 | 240, 250 | negdid 10018 |
. . . 4
 
      coeff                   coeff    
          |
252 | 240, 245 | mulcld 9681 |
. . . . . . 7
 
          |
253 | 252, 244,
245, 249 | divdird 10443 |
. . . . . 6
 
           coeff                             coeff               |
254 | | nnm1nn0 10935 |
. . . . . . . . . . 11
 
   |
255 | 5, 254 | syl 17 |
. . . . . . . . . 10
     |
256 | 255 | adantr 472 |
. . . . . . . . 9
 
 
   |
257 | 176, 177 | coemul 23285 |
. . . . . . . . 9
          Poly  Poly      coeff                            coeff              coeff            |
258 | 69, 32, 256, 257 | syl3anc 1292 |
. . . . . . . 8
 
  coeff               
  
         coeff              coeff            |
259 | 159 | fveq1d 5881 |
. . . . . . . 8
 
        coeff                    |
260 | | 1e0p1 11102 |
. . . . . . . . . . . 12
   |
261 | 260 | oveq2i 6319 |
. . . . . . . . . . 11
           |
262 | 261 | sumeq1i 13841 |
. . . . . . . . . 10
        coeff              coeff                    coeff              coeff           |
263 | | 0nn0 10908 |
. . . . . . . . . . . . 13
 |
264 | | nn0uz 11217 |
. . . . . . . . . . . . 13
     |
265 | 263, 264 | eleqtri 2547 |
. . . . . . . . . . . 12
     |
266 | 265 | a1i 11 |
. . . . . . . . . . 11
 
       |
267 | 261 | eleq2i 2541 |
. . . . . . . . . . . 12
    
        |
268 | 176 | coef3 23265 |
. . . . . . . . . . . . . . 15
         Poly 
coeff                |
269 | 69, 268 | syl 17 |
. . . . . . . . . . . . . 14
 
 coeff                |
270 | | elfznn0 11913 |
. . . . . . . . . . . . . 14
       |
271 | | ffvelrn 6035 |
. . . . . . . . . . . . . 14
  coeff                coeff               |
272 | 269, 270,
271 | syl2an 485 |
. . . . . . . . . . . . 13
          coeff               |
273 | 2 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . . 20
         |
274 | | pncan 9901 |
. . . . . . . . . . . . . . . . . . . . 21
 
       |
275 | 102, 101,
274 | sylancl 675 |
. . . . . . . . . . . . . . . . . . . 20
       |
276 | 273, 275 | eqtr3d 2507 |
. . . . . . . . . . . . . . . . . . 19
     |
277 | 276 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
 
 
   |
278 | 3 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
 
   |
279 | 277, 278 | eqeltrd 2549 |
. . . . . . . . . . . . . . . . 17
 
 
   |
280 | | nnuz 11218 |
. . . . . . . . . . . . . . . . 17
     |
281 | 279, 280 | syl6eleq 2559 |
. . . . . . . . . . . . . . . 16
 
 
       |
282 | | fzss2 11864 |
. . . . . . . . . . . . . . . 16
      
       
    |
283 | 281, 282 | syl 17 |
. . . . . . . . . . . . . . 15
 
        
    |
284 | 283 | sselda 3418 |
. . . . . . . . . . . . . 14
            
    |
285 | | fznn0sub 11857 |
. . . . . . . . . . . . . . 15
             |
286 | | ffvelrn 6035 |
. . . . . . . . . . . . . . 15
  coeff            coeff     
     |
287 | 231, 285,
286 | syl2an 485 |
. . . . . . . . . . . . . 14
       
    coeff           |
288 | 284, 287 | syldan 478 |
. . . . . . . . . . . . 13
          coeff           |
289 | 272, 288 | mulcld 9681 |
. . . . . . . . . . . 12
           coeff              coeff            |
290 | 267, 289 | sylan2br 484 |
. . . . . . . . . . 11
             coeff              coeff            |
291 | | id 22 |
. . . . . . . . . . . . . 14
       |
292 | 291, 260 | syl6eqr 2523 |
. . . . . . . . . . . . 13
     |
293 | 292 | fveq2d 5883 |
. . . . . . . . . . . 12
    coeff              coeff               |
294 | 292 | oveq2d 6324 |
. . . . . . . . . . . . 13
             |
295 | 294 | fveq2d 5883 |
. . . . . . . . . . . 12
    coeff          coeff           |
296 | 293, 295 | oveq12d 6326 |
. . . . . . . . . . 11
     coeff              coeff            coeff              coeff            |
297 | 266, 290,
296 | fsump1 13894 |
. . . . . . . . . 10
 
           coeff              coeff                   coeff              coeff            coeff              coeff             |
298 | 262, 297 | syl5eq 2517 |
. . . . . . . . 9
 
         coeff              coeff                   coeff              coeff            coeff              coeff             |
299 | | eldifn 3545 |
. . . . . . . . . . . . . 14
            
      |
300 | 299 | adantl 473 |
. . . . . . . . . . . . 13
                
      |
301 | | eldifi 3544 |
. . . . . . . . . . . . . . . . 17
                
    |
302 | | elfznn0 11913 |
. . . . . . . . . . . . . . . . 17
         |
303 | 301, 302 | syl 17 |
. . . . . . . . . . . . . . . 16
               |
304 | 176, 169 | dgrub 23267 |
. . . . . . . . . . . . . . . . 17
          Poly   coeff             
deg            |
305 | 304 | 3expia 1233 |
. . . . . . . . . . . . . . . 16
          Poly     coeff            
deg             |
306 | 69, 303, 305 | syl2an 485 |
. . . . . . . . . . . . . . 15
                
  coeff            
deg             |
307 | | elfzuz 11822 |
. . . . . . . . . . . . . . . . . . 19
             |
308 | 301, 307 | syl 17 |
. . . . . . . . . . . . . . . . . 18
                   |
309 | 308 | adantl 473 |
. . . . . . . . . . . . . . . . 17
                
      |
310 | | 1z 10991 |
. . . . . . . . . . . . . . . . 17
 |
311 | | elfz5 11818 |
. . . . . . . . . . . . . . . . 17
           
   |
312 | 309, 310,
311 | sylancl 675 |
. . . . . . . . . . . . . . . 16
                
        |
313 | 161 | breq2d 4407 |
. . . . . . . . . . . . . . . . 17
 
 
deg         
   |
314 | 313 | adantr 472 |
. . . . . . . . . . . . . . . 16
                
 deg         
   |
315 | 312, 314 | bitr4d 264 |
. . . . . . . . . . . . . . 15
                
     deg             |
316 | 306, 315 | sylibrd 242 |
. . . . . . . . . . . . . 14
                
  coeff                    |
317 | 316 | necon1bd 2661 |
. . . . . . . . . . . . 13
                

     coeff                |
318 | 300, 317 | mpd 15 |
. . . . . . . . . . . 12
                
 coeff               |
319 | 318 | oveq1d 6323 |
. . . . . . . . . . 11
                
  coeff              coeff            coeff            |
320 | 301, 287 | sylan2 482 |
. . . . . . . . . . . 12
                
 coeff           |
321 | 320 | mul02d 9849 |
. . . . . . . . . . 11
                
  coeff            |
322 | 319, 321 | eqtrd 2505 |
. . . . . . . . . 10
                
  coeff              coeff            |
323 | | fzfid 12224 |
. . . . . . . . . 10
 
         |
324 | 283, 289,
322, 323 | fsumss 13868 |
. . . . . . . . 9
 
         coeff              coeff                    coeff              coeff            |
325 | | 0z 10972 |
. . . . . . . . . . . 12
 |
326 | 189 | fveq1d 5881 |
. . . . . . . . . . . . . . 15
 
  coeff               coeff    coeff            |
327 | | coeidp 23296 |
. . . . . . . . . . . . . . . . . . . 20

 coeff             |
328 | 162 | nesymi 2700 |
. . . . . . . . . . . . . . . . . . . . 21
 |
329 | 328 | iffalsei 3882 |
. . . . . . . . . . . . . . . . . . . 20
      |
330 | 327, 329 | syl6eq 2521 |
. . . . . . . . . . . . . . . . . . 19

 coeff        |
331 | 330 | adantl 473 |
. . . . . . . . . . . . . . . . . 18
      coeff        |
332 | | 0cn 9653 |
. . . . . . . . . . . . . . . . . . . . 21
 |
333 | | vex 3034 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
334 | 333 | fvconst2 6136 |
. . . . . . . . . . . . . . . . . . . . 21
           |
335 | 332, 334 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
         |
336 | 187 | coefv0 23281 |
. . . . . . . . . . . . . . . . . . . . 21
     Poly           coeff           |
337 | 185, 336 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
 
          coeff           |
338 | 335, 337 | syl5reqr 2520 |
. . . . . . . . . . . . . . . . . . 19
 
  coeff           |
339 | 338 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
      coeff           |
340 | 195, 198,
200, 200, 201, 331, 339 | ofval 6559 |
. . . . . . . . . . . . . . . . 17
       coeff    coeff              |
341 | 263, 340 | mpan2 685 |
. . . . . . . . . . . . . . . 16
 
   coeff    coeff              |
342 | | df-neg 9883 |
. . . . . . . . . . . . . . . 16
    |
343 | 341, 342 | syl6eqr 2523 |
. . . . . . . . . . . . . . 15
 
   coeff    coeff             |
344 | 326, 343 | eqtrd 2505 |
. . . . . . . . . . . . . 14
 
  coeff                |
345 | 277 | oveq1d 6323 |
. . . . . . . . . . . . . . . . 17
 
         |
346 | 103 | subid1d 9994 |
. . . . . . . . . . . . . . . . 17
 
 
   |
347 | 345, 346,
31 | 3eqtrd 2509 |
. . . . . . . . . . . . . . . 16
 
     deg    |
348 | 347 | fveq2d 5883 |
. . . . . . . . . . . . . . 15
 
  coeff          coeff    deg     |
349 | 348, 235 | eqtr4d 2508 |
. . . . . . . . . . . . . 14
 
  coeff               |
350 | 344, 349 | oveq12d 6326 |
. . . . . . . . . . . . 13
 
   coeff              coeff                   |
351 | 350, 252 | eqeltrd 2549 |
. . . . . . . . . . . 12
 
   coeff              coeff            |
352 | | fveq2 5879 |
. . . . . . . . . . . . . 14
  coeff              coeff               |
353 | | oveq2 6316 |
. . . . . . . . . . . . . . 15
           |
354 | 353 | fveq2d 5883 |
. . . . . . . . . . . . . 14
  coeff          coeff           |
355 | 352, 354 | oveq12d 6326 |
. . . . . . . . . . . . 13
   coeff              coeff            coeff              coeff            |
356 | 355 | fsum1 13885 |
. . . . . . . . . . . 12
    coeff              coeff                   coeff              coeff            coeff              coeff            |
357 | 325, 351,
356 | sylancr 676 |
. . . . . . . . . . 11
 
         coeff              coeff            coeff              coeff            |
358 | 357, 350 | eqtrd 2505 |
. . . . . . . . . 10
 
         coeff              coeff                   |
359 | 277 | oveq1d 6323 |
. . . . . . . . . . . . 13
 
         |
360 | 359 | fveq2d 5883 |
. . . . . . . . . . . 12
 
  coeff          coeff         |
361 | 227, 360 | oveq12d 6326 |
. . . . . . . . . . 11
 
   coeff              coeff            coeff    
     |
362 | 244 | mulid2d 9679 |
. . . . . . . . . . 11
 
   coeff    
    coeff         |
363 | 361, 362 | eqtrd 2505 |
. . . . . . . . . 10
 
   coeff              coeff           coeff         |
364 | 358, 363 | oveq12d 6326 |
. . . . . . . . 9
 
          coeff              coeff            coeff              coeff                    coeff          |
365 | 298, 324,
364 | 3eqtr3rd 2514 |
. . . . . . . 8
 
          coeff    
   
         coeff              coeff            |
366 | 258, 259,
365 | 3eqtr4rd 2516 |
. . . . . . 7
 
          coeff    
           |
367 | 366 | oveq1d 6323 |
. . . . . 6
 
           coeff                 
         |
368 | 240, 245,
249 | divcan4d 10411 |
. . . . . . 7
 
                 |
369 | 368 | oveq1d 6323 |
. . . . . 6
 
                 coeff                 coeff               |
370 | 253, 367,
369 | 3eqtr3rd 2514 |
. . . . 5
 
     coeff                 
         |
371 | 370 | negeqd 9889 |
. . . 4
 
      coeff                  
         |
372 | 251, 371 | eqtr3d 2507 |
. . 3
 
   
   coeff                            |
373 | 129, 239,
372 | 3eqtrd 2509 |
. 2
 
 
     
         |
374 | 25, 373 | exlimddv 1789 |
1
 
               |