Step | Hyp | Ref
| Expression |
1 | | vieta1.5 |
. . . . 5
       |
2 | | vieta1lem.7 |
. . . . . . 7
     |
3 | | vieta1lem.6 |
. . . . . . . 8
   |
4 | 3 | peano2nnd 10626 |
. . . . . . 7
     |
5 | 2, 4 | eqeltrrd 2530 |
. . . . . 6
   |
6 | 5 | nnne0d 10654 |
. . . . 5
   |
7 | 1, 6 | eqnetrd 2691 |
. . . 4
       |
8 | | vieta1.4 |
. . . . . . . 8
 Poly    |
9 | | vieta1.2 |
. . . . . . . . . 10
deg   |
10 | 9, 6 | syl5eqner 2699 |
. . . . . . . . 9
 deg    |
11 | | fveq2 5865 |
. . . . . . . . . . 11
  deg  deg     |
12 | | dgr0 23216 |
. . . . . . . . . . 11
deg    |
13 | 11, 12 | syl6eq 2501 |
. . . . . . . . . 10
  deg    |
14 | 13 | necon3i 2656 |
. . . . . . . . 9
 deg 
   |
15 | 10, 14 | syl 17 |
. . . . . . . 8
    |
16 | | vieta1.3 |
. . . . . . . . 9
        |
17 | 16 | fta1 23261 |
. . . . . . . 8
  Poly        
deg     |
18 | 8, 15, 17 | syl2anc 667 |
. . . . . . 7
     
deg     |
19 | 18 | simpld 461 |
. . . . . 6
   |
20 | | hasheq0 12544 |
. . . . . 6
     
   |
21 | 19, 20 | syl 17 |
. . . . 5
         |
22 | 21 | necon3bid 2668 |
. . . 4
         |
23 | 7, 22 | mpbid 214 |
. . 3
   |
24 | | n0 3741 |
. . 3
    |
25 | 23, 24 | sylib 200 |
. 2
    |
26 | | incom 3625 |
. . . . 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 23263 |
. . . . . . . . . 10
 
 
Poly  deg     |
31 | 30 | simprd 465 |
. . . . . . . . 9
 
 deg    |
32 | 30 | simpld 461 |
. . . . . . . . . . 11
 
 Poly    |
33 | | dgrcl 23187 |
. . . . . . . . . . 11
 Poly  deg    |
34 | 32, 33 | syl 17 |
. . . . . . . . . 10
 
 deg    |
35 | 34 | nn0red 10926 |
. . . . . . . . 9
 
 deg    |
36 | 31, 35 | eqeltrd 2529 |
. . . . . . . 8
 
   |
37 | 36 | ltp1d 10537 |
. . . . . . . 8
 
     |
38 | 36, 37 | gtned 9770 |
. . . . . . 7
 
 
   |
39 | | snssi 4116 |
. . . . . . . . . . 11
                   |
40 | | ssequn1 3604 |
. . . . . . . . . . 11
         
                    |
41 | 39, 40 | sylib 200 |
. . . . . . . . . 10
                            |
42 | 41 | fveq2d 5869 |
. . . . . . . . 9
                                    |
43 | 8 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 
 Poly    |
44 | | cnvimass 5188 |
. . . . . . . . . . . . . . . . . . . . 21
        |
45 | 16, 44 | eqsstri 3462 |
. . . . . . . . . . . . . . . . . . . 20
 |
46 | | plyf 23152 |
. . . . . . . . . . . . . . . . . . . . 21
 Poly 
      |
47 | | fdm 5733 |
. . . . . . . . . . . . . . . . . . . . 21
       |
48 | 8, 46, 47 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
   |
49 | 45, 48 | syl5sseq 3480 |
. . . . . . . . . . . . . . . . . . 19

  |
50 | 49 | sselda 3432 |
. . . . . . . . . . . . . . . . . 18
 
   |
51 | 16 | eleq2i 2521 |
. . . . . . . . . . . . . . . . . . . 20

         |
52 | | ffn 5728 |
. . . . . . . . . . . . . . . . . . . . 21
       |
53 | | fniniseg 6003 |
. . . . . . . . . . . . . . . . . . . . 21
        
         |
54 | 8, 46, 52, 53 | 4syl 19 |
. . . . . . . . . . . . . . . . . . . 20
        
         |
55 | 51, 54 | syl5bb 261 |
. . . . . . . . . . . . . . . . . . 19
           |
56 | 55 | simplbda 630 |
. . . . . . . . . . . . . . . . . 18
 
       |
57 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . 19
   
             |
58 | 57 | facth 23259 |
. . . . . . . . . . . . . . . . . 18
  Poly           
      quot             |
59 | 43, 50, 56, 58 | syl3anc 1268 |
. . . . . . . . . . . . . . . . 17
 
     
      quot             |
60 | 29 | oveq2i 6301 |
. . . . . . . . . . . . . . . . 17
                      quot            |
61 | 59, 60 | syl6eqr 2503 |
. . . . . . . . . . . . . . . 16
 
     
        |
62 | 61 | cnveqd 5010 |
. . . . . . . . . . . . . . 15
 
 
              |
63 | 62 | imaeq1d 5167 |
. . . . . . . . . . . . . 14
 
              
             |
64 | 16, 63 | syl5eq 2497 |
. . . . . . . . . . . . 13
 
                     |
65 | | cnex 9620 |
. . . . . . . . . . . . . . 15
 |
66 | 65 | a1i 11 |
. . . . . . . . . . . . . 14
 
   |
67 | 57 | plyremlem 23257 |
. . . . . . . . . . . . . . . . 17
          Poly  deg                              |
68 | 50, 67 | syl 17 |
. . . . . . . . . . . . . . . 16
 
          Poly  deg                              |
69 | 68 | simp1d 1020 |
. . . . . . . . . . . . . . 15
 
         Poly    |
70 | | plyf 23152 |
. . . . . . . . . . . . . . 15
         Poly 
   
          |
71 | 69, 70 | syl 17 |
. . . . . . . . . . . . . 14
 
               |
72 | | plyf 23152 |
. . . . . . . . . . . . . . 15
 Poly        |
73 | 32, 72 | syl 17 |
. . . . . . . . . . . . . 14
 
       |
74 | | ofmulrt 23235 |
. . . . . . . . . . . . . 14
                  
                                            |
75 | 66, 71, 73, 74 | syl3anc 1268 |
. . . . . . . . . . . . 13
 
       
                                     |
76 | 68 | simp3d 1022 |
. . . . . . . . . . . . . 14
 
                    |
77 | 76 | uneq1d 3587 |
. . . . . . . . . . . . 13
 
       
                              |
78 | 64, 75, 77 | 3eqtrd 2489 |
. . . . . . . . . . . 12
 
              |
79 | 78 | fveq2d 5869 |
. . . . . . . . . . 11
 
                      |
80 | 1, 2 | eqtr4d 2488 |
. . . . . . . . . . . 12
         |
81 | 80 | adantr 467 |
. . . . . . . . . . 11
 
         |
82 | 79, 81 | eqtr3d 2487 |
. . . . . . . . . 10
 
                    |
83 | 15 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 
    |
84 | 61, 83 | eqnetrrd 2692 |
. . . . . . . . . . . . . . . . 17
 
               |
85 | | plymul0or 23234 |
. . . . . . . . . . . . . . . . . . 19
          Poly  Poly  
            
               |
86 | 69, 32, 85 | syl2anc 667 |
. . . . . . . . . . . . . . . . . 18
 
             
               |
87 | 86 | necon3abid 2660 |
. . . . . . . . . . . . . . . . 17
 
             
               |
88 | 84, 87 | mpbid 214 |
. . . . . . . . . . . . . . . 16
 
               |
89 | | neanior 2716 |
. . . . . . . . . . . . . . . 16
            
              |
90 | 88, 89 | sylibr 216 |
. . . . . . . . . . . . . . 15
 
               |
91 | 90 | simprd 465 |
. . . . . . . . . . . . . 14
 
    |
92 | | eqid 2451 |
. . . . . . . . . . . . . . 15
               |
93 | 92 | fta1 23261 |
. . . . . . . . . . . . . 14
  Poly 
                    
deg     |
94 | 32, 91, 93 | syl2anc 667 |
. . . . . . . . . . . . 13
 
                   
deg     |
95 | 94 | simprd 465 |
. . . . . . . . . . . 12
 
           
deg    |
96 | 95, 31 | breqtrrd 4429 |
. . . . . . . . . . 11
 
           
  |
97 | | snfi 7650 |
. . . . . . . . . . . . . 14
   |
98 | 94 | simpld 461 |
. . . . . . . . . . . . . 14
 
          |
99 | | hashun2 12562 |
. . . . . . . . . . . . . 14
                                                |
100 | 97, 98, 99 | sylancr 669 |
. . . . . . . . . . . . 13
 
                                     |
101 | | ax-1cn 9597 |
. . . . . . . . . . . . . . 15
 |
102 | 3 | nncnd 10625 |
. . . . . . . . . . . . . . . 16
   |
103 | 102 | adantr 467 |
. . . . . . . . . . . . . . 15
 
   |
104 | | addcom 9819 |
. . . . . . . . . . . . . . 15
 
       |
105 | 101, 103,
104 | sylancr 669 |
. . . . . . . . . . . . . 14
 
       |
106 | 82, 105 | eqtr4d 2488 |
. . . . . . . . . . . . 13
 
                    |
107 | | hashsng 12549 |
. . . . . . . . . . . . . . 15
         |
108 | 107 | adantl 468 |
. . . . . . . . . . . . . 14
 
         |
109 | 108 | oveq1d 6305 |
. . . . . . . . . . . . 13
 
                                   |
110 | 100, 106,
109 | 3brtr3d 4432 |
. . . . . . . . . . . 12
 
                  |
111 | | hashcl 12538 |
. . . . . . . . . . . . . . 15
                     |
112 | 98, 111 | syl 17 |
. . . . . . . . . . . . . 14
 
              |
113 | 112 | nn0red 10926 |
. . . . . . . . . . . . 13
 
              |
114 | | 1red 9658 |
. . . . . . . . . . . . 13
 
   |
115 | 36, 113, 114 | leadd2d 10208 |
. . . . . . . . . . . 12
 
            
                  |
116 | 110, 115 | mpbird 236 |
. . . . . . . . . . 11
 
              |
117 | 113, 36 | letri3d 9777 |
. . . . . . . . . . 11
 
                        
               |
118 | 96, 116, 117 | mpbir2and 933 |
. . . . . . . . . 10
 
              |
119 | 82, 118 | eqeq12d 2466 |
. . . . . . . . 9
 
                           
     |
120 | 42, 119 | syl5ib 223 |
. . . . . . . 8
 
         
    |
121 | 120 | necon3ad 2637 |
. . . . . . 7
 
   
          |
122 | 38, 121 | mpd 15 |
. . . . . 6
 

         |
123 | | disjsn 4032 |
. . . . . 6
           
         |
124 | 122, 123 | sylibr 216 |
. . . . 5
 
              |
125 | 26, 124 | syl5eq 2497 |
. . . 4
 
              |
126 | 19 | adantr 467 |
. . . 4
 
   |
127 | 49 | adantr 467 |
. . . . 5
 
   |
128 | 127 | sselda 3432 |
. . . 4
       |
129 | 125, 78, 126, 128 | fsumsplit 13806 |
. . 3
 
 
                 |
130 | | id 22 |
. . . . . . 7
   |
131 | 130 | sumsn 13807 |
. . . . . 6
 
 
     |
132 | 50, 50, 131 | syl2anc 667 |
. . . . 5
 
       |
133 | 50 | negnegd 9977 |
. . . . 5
 
     |
134 | 132, 133 | eqtr4d 2488 |
. . . 4
 
         |
135 | 118, 31 | eqtrd 2485 |
. . . . . 6
 
            deg    |
136 | 28 | adantr 467 |
. . . . . . 7
 
  Poly     deg             deg               coeff     deg     coeff    deg       |
137 | | fveq2 5865 |
. . . . . . . . . . 11
 deg  deg    |
138 | 137 | eqeq2d 2461 |
. . . . . . . . . 10
 
deg 
deg     |
139 | | cnveq 5008 |
. . . . . . . . . . . . 13
 
   |
140 | 139 | imaeq1d 5167 |
. . . . . . . . . . . 12
                 |
141 | 140 | fveq2d 5869 |
. . . . . . . . . . 11
                         |
142 | 141, 137 | eqeq12d 2466 |
. . . . . . . . . 10
             deg             deg     |
143 | 138, 142 | anbi12d 717 |
. . . . . . . . 9
   deg             deg    deg             deg      |
144 | 140 | sumeq1d 13767 |
. . . . . . . . . 10
                     |
145 | | fveq2 5865 |
. . . . . . . . . . . . 13
 coeff  coeff    |
146 | 137 | oveq1d 6305 |
. . . . . . . . . . . . 13
  deg    deg     |
147 | 145, 146 | fveq12d 5871 |
. . . . . . . . . . . 12
  coeff     deg     coeff     deg      |
148 | 145, 137 | fveq12d 5871 |
. . . . . . . . . . . 12
  coeff    deg    coeff    deg     |
149 | 147, 148 | oveq12d 6308 |
. . . . . . . . . . 11
   coeff     deg     coeff    deg      coeff     deg     coeff    deg      |
150 | 149 | negeqd 9869 |
. . . . . . . . . 10
    coeff     deg     coeff    deg       coeff     deg     coeff    deg      |
151 | 144, 150 | eqeq12d 2466 |
. . . . . . . . 9
              coeff     deg     coeff    deg                coeff     deg     coeff    deg       |
152 | 143, 151 | imbi12d 322 |
. . . . . . . 8
    deg             deg               coeff     deg     coeff    deg    
 
deg 
           deg  
            coeff     deg     coeff    deg        |
153 | 152 | rspcv 3146 |
. . . . . . 7
 Poly    Poly     deg             deg               coeff     deg     coeff    deg       deg             deg  
            coeff     deg     coeff    deg        |
154 | 32, 136, 153 | sylc 62 |
. . . . . 6
 
   deg             deg  
            coeff     deg     coeff    deg       |
155 | 31, 135, 154 | mp2and 685 |
. . . . 5
 
             coeff     deg     coeff    deg      |
156 | 31 | oveq1d 6305 |
. . . . . . . 8
 
 
  deg     |
157 | 156 | fveq2d 5869 |
. . . . . . 7
 
  coeff        coeff     deg      |
158 | 61 | fveq2d 5869 |
. . . . . . . . . 10
 
 coeff  coeff               |
159 | 27, 158 | syl5eq 2497 |
. . . . . . . . 9
 
 coeff               |
160 | 61 | fveq2d 5869 |
. . . . . . . . . . 11
 
 deg  deg     
         |
161 | 68 | simp2d 1021 |
. . . . . . . . . . . . . 14
 
 deg            |
162 | | ax-1ne0 9608 |
. . . . . . . . . . . . . . 15
 |
163 | 162 | a1i 11 |
. . . . . . . . . . . . . 14
 
   |
164 | 161, 163 | eqnetrd 2691 |
. . . . . . . . . . . . 13
 
 deg            |
165 | | fveq2 5865 |
. . . . . . . . . . . . . . 15
          deg          deg     |
166 | 165, 12 | syl6eq 2501 |
. . . . . . . . . . . . . 14
          deg            |
167 | 166 | necon3i 2656 |
. . . . . . . . . . . . 13
 deg         
           |
168 | 164, 167 | syl 17 |
. . . . . . . . . . . 12
 
            |
169 | | eqid 2451 |
. . . . . . . . . . . . 13
deg          deg           |
170 | | eqid 2451 |
. . . . . . . . . . . . 13
deg  deg   |
171 | 169, 170 | dgrmul 23224 |
. . . . . . . . . . . 12
           Poly             Poly     deg              deg          deg     |
172 | 69, 168, 32, 91, 171 | syl22anc 1269 |
. . . . . . . . . . 11
 
 deg              deg          deg     |
173 | 160, 172 | eqtrd 2485 |
. . . . . . . . . 10
 
 deg   deg          deg     |
174 | 9, 173 | syl5eq 2497 |
. . . . . . . . 9
 
  deg          deg     |
175 | 159, 174 | fveq12d 5871 |
. . . . . . . 8
 
      coeff                deg          deg      |
176 | | eqid 2451 |
. . . . . . . . . 10
coeff          coeff           |
177 | | eqid 2451 |
. . . . . . . . . 10
coeff  coeff   |
178 | 176, 177,
169, 170 | coemulhi 23208 |
. . . . . . . . 9
          Poly  Poly  
 coeff                deg          deg      coeff            deg            coeff    deg      |
179 | 69, 32, 178 | syl2anc 667 |
. . . . . . . 8
 
  coeff                deg          deg      coeff            deg            coeff    deg      |
180 | 161 | fveq2d 5869 |
. . . . . . . . . . 11
 
  coeff            deg            coeff               |
181 | | ssid 3451 |
. . . . . . . . . . . . . . 15
 |
182 | | plyid 23163 |
. . . . . . . . . . . . . . 15
 
 
Poly    |
183 | 181, 101,
182 | mp2an 678 |
. . . . . . . . . . . . . 14
 Poly   |
184 | | plyconst 23160 |
. . . . . . . . . . . . . . 15
 
     Poly    |
185 | 181, 50, 184 | sylancr 669 |
. . . . . . . . . . . . . 14
 
     Poly    |
186 | | eqid 2451 |
. . . . . . . . . . . . . . 15
coeff   coeff    |
187 | | eqid 2451 |
. . . . . . . . . . . . . . 15
coeff 
    coeff       |
188 | 186, 187 | coesub 23211 |
. . . . . . . . . . . . . 14
   Poly      Poly   coeff           coeff    coeff         |
189 | 183, 185,
188 | sylancr 669 |
. . . . . . . . . . . . 13
 
 coeff           coeff    coeff         |
190 | 189 | fveq1d 5867 |
. . . . . . . . . . . 12
 
  coeff               coeff    coeff            |
191 | | 1nn0 10885 |
. . . . . . . . . . . . . 14
 |
192 | 186 | coef3 23186 |
. . . . . . . . . . . . . . . . 17
  Poly 
coeff         |
193 | | ffn 5728 |
. . . . . . . . . . . . . . . . 17
 coeff       coeff     |
194 | 183, 192,
193 | mp2b 10 |
. . . . . . . . . . . . . . . 16
coeff    |
195 | 194 | a1i 11 |
. . . . . . . . . . . . . . 15
 
 coeff     |
196 | 187 | coef3 23186 |
. . . . . . . . . . . . . . . 16
     Poly  coeff            |
197 | | ffn 5728 |
. . . . . . . . . . . . . . . 16
 coeff          coeff        |
198 | 185, 196,
197 | 3syl 18 |
. . . . . . . . . . . . . . 15
 
 coeff        |
199 | | nn0ex 10875 |
. . . . . . . . . . . . . . . 16
 |
200 | 199 | a1i 11 |
. . . . . . . . . . . . . . 15
 
   |
201 | | inidm 3641 |
. . . . . . . . . . . . . . 15
   |
202 | | coeidp 23217 |
. . . . . . . . . . . . . . . . 17

 coeff             |
203 | 202 | adantl 468 |
. . . . . . . . . . . . . . . 16
      coeff             |
204 | | eqid 2451 |
. . . . . . . . . . . . . . . . 17
 |
205 | 204 | iftruei 3888 |
. . . . . . . . . . . . . . . 16
      |
206 | 203, 205 | syl6eq 2501 |
. . . . . . . . . . . . . . 15
      coeff        |
207 | | 0lt1 10136 |
. . . . . . . . . . . . . . . . . 18
 |
208 | | 0re 9643 |
. . . . . . . . . . . . . . . . . . 19
 |
209 | | 1re 9642 |
. . . . . . . . . . . . . . . . . . 19
 |
210 | 208, 209 | ltnlei 9755 |
. . . . . . . . . . . . . . . . . 18

  |
211 | 207, 210 | mpbi 212 |
. . . . . . . . . . . . . . . . 17
 |
212 | 50 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
       |
213 | | 0dgr 23199 |
. . . . . . . . . . . . . . . . . . 19
 deg        |
214 | 212, 213 | syl 17 |
. . . . . . . . . . . . . . . . . 18
     deg        |
215 | 214 | breq2d 4414 |
. . . . . . . . . . . . . . . . 17
     
deg     
   |
216 | 211, 215 | mtbiri 305 |
. . . . . . . . . . . . . . . 16
     deg        |
217 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . . 20
deg 
    deg       |
218 | 187, 217 | dgrub 23188 |
. . . . . . . . . . . . . . . . . . 19
      Poly 
 coeff          deg        |
219 | 218 | 3expia 1210 |
. . . . . . . . . . . . . . . . . 18
      Poly 
   coeff        
deg         |
220 | 185, 219 | sylan 474 |
. . . . . . . . . . . . . . . . 17
       coeff        
deg         |
221 | 220 | necon1bd 2642 |
. . . . . . . . . . . . . . . 16
     
deg 
     coeff            |
222 | 216, 221 | mpd 15 |
. . . . . . . . . . . . . . 15
      coeff           |
223 | 195, 198,
200, 200, 201, 206, 222 | ofval 6540 |
. . . . . . . . . . . . . 14
       coeff    coeff              |
224 | 191, 223 | mpan2 677 |
. . . . . . . . . . . . 13
 
   coeff    coeff              |
225 | | 1m0e1 10720 |
. . . . . . . . . . . . 13
   |
226 | 224, 225 | syl6eq 2501 |
. . . . . . . . . . . 12
 
   coeff    coeff            |
227 | 190, 226 | eqtrd 2485 |
. . . . . . . . . . 11
 
  coeff               |
228 | 180, 227 | eqtrd 2485 |
. . . . . . . . . 10
 
  coeff            deg             |
229 | 228 | oveq1d 6305 |
. . . . . . . . 9
 
   coeff            deg            coeff    deg      coeff    deg      |
230 | 177 | coef3 23186 |
. . . . . . . . . . . 12
 Poly  coeff        |
231 | 32, 230 | syl 17 |
. . . . . . . . . . 11
 
 coeff        |
232 | 231, 34 | ffvelrnd 6023 |
. . . . . . . . . 10
 
  coeff    deg     |
233 | 232 | mulid2d 9661 |
. . . . . . . . 9
 
   coeff    deg     coeff    deg     |
234 | 229, 233 | eqtrd 2485 |
. . . . . . . 8
 
   coeff            deg            coeff    deg     coeff    deg     |
235 | 175, 179,
234 | 3eqtrd 2489 |
. . . . . . 7
 
      coeff    deg     |
236 | 157, 235 | oveq12d 6308 |
. . . . . 6
 
   coeff              coeff     deg     coeff    deg      |
237 | 236 | negeqd 9869 |
. . . . 5
 
    coeff               coeff     deg     coeff    deg      |
238 | 155, 237 | eqtr4d 2488 |
. . . 4
 
             coeff              |
239 | 134, 238 | oveq12d 6308 |
. . 3
 
                      coeff    
          |
240 | 50 | negcld 9973 |
. . . . 5
 
    |
241 | | nnm1nn0 10911 |
. . . . . . . . 9
 
   |
242 | 3, 241 | syl 17 |
. . . . . . . 8
     |
243 | 242 | adantr 467 |
. . . . . . 7
 
 
   |
244 | 231, 243 | ffvelrnd 6023 |
. . . . . 6
 
  coeff         |
245 | 235, 232 | eqeltrd 2529 |
. . . . . 6
 
       |
246 | 9, 27 | dgreq0 23219 |
. . . . . . . . 9
 Poly 
 
       |
247 | 43, 246 | syl 17 |
. . . . . . . 8
 
 
        |
248 | 247 | necon3bid 2668 |
. . . . . . 7
 
  
       |
249 | 83, 248 | mpbid 214 |
. . . . . 6
 
       |
250 | 244, 245,
249 | divcld 10383 |
. . . . 5
 
   coeff              |
251 | 240, 250 | negdid 9999 |
. . . 4
 
      coeff                   coeff    
          |
252 | 240, 245 | mulcld 9663 |
. . . . . . 7
 
          |
253 | 252, 244,
245, 249 | divdird 10421 |
. . . . . 6
 
           coeff                             coeff               |
254 | | nnm1nn0 10911 |
. . . . . . . . . . 11
 
   |
255 | 5, 254 | syl 17 |
. . . . . . . . . 10
     |
256 | 255 | adantr 467 |
. . . . . . . . 9
 
 
   |
257 | 176, 177 | coemul 23206 |
. . . . . . . . 9
          Poly  Poly      coeff                            coeff              coeff            |
258 | 69, 32, 256, 257 | syl3anc 1268 |
. . . . . . . 8
 
  coeff               
  
         coeff              coeff            |
259 | 159 | fveq1d 5867 |
. . . . . . . 8
 
        coeff                    |
260 | | 1e0p1 11079 |
. . . . . . . . . . . 12
   |
261 | 260 | oveq2i 6301 |
. . . . . . . . . . 11
           |
262 | 261 | sumeq1i 13764 |
. . . . . . . . . 10
        coeff              coeff                    coeff              coeff           |
263 | | 0nn0 10884 |
. . . . . . . . . . . . 13
 |
264 | | nn0uz 11193 |
. . . . . . . . . . . . 13
     |
265 | 263, 264 | eleqtri 2527 |
. . . . . . . . . . . 12
     |
266 | 265 | a1i 11 |
. . . . . . . . . . 11
 
       |
267 | 261 | eleq2i 2521 |
. . . . . . . . . . . 12
    
        |
268 | 176 | coef3 23186 |
. . . . . . . . . . . . . . 15
         Poly 
coeff                |
269 | 69, 268 | syl 17 |
. . . . . . . . . . . . . 14
 
 coeff                |
270 | | elfznn0 11887 |
. . . . . . . . . . . . . 14
       |
271 | | ffvelrn 6020 |
. . . . . . . . . . . . . 14
  coeff                coeff               |
272 | 269, 270,
271 | syl2an 480 |
. . . . . . . . . . . . 13
          coeff               |
273 | 2 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . . . 20
         |
274 | | pncan 9881 |
. . . . . . . . . . . . . . . . . . . . 21
 
       |
275 | 102, 101,
274 | sylancl 668 |
. . . . . . . . . . . . . . . . . . . 20
       |
276 | 273, 275 | eqtr3d 2487 |
. . . . . . . . . . . . . . . . . . 19
     |
277 | 276 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 
 
   |
278 | 3 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 
   |
279 | 277, 278 | eqeltrd 2529 |
. . . . . . . . . . . . . . . . 17
 
 
   |
280 | | nnuz 11194 |
. . . . . . . . . . . . . . . . 17
     |
281 | 279, 280 | syl6eleq 2539 |
. . . . . . . . . . . . . . . 16
 
 
       |
282 | | fzss2 11838 |
. . . . . . . . . . . . . . . 16
      
       
    |
283 | 281, 282 | syl 17 |
. . . . . . . . . . . . . . 15
 
        
    |
284 | 283 | sselda 3432 |
. . . . . . . . . . . . . 14
            
    |
285 | | fznn0sub 11831 |
. . . . . . . . . . . . . . 15
             |
286 | | ffvelrn 6020 |
. . . . . . . . . . . . . . 15
  coeff            coeff     
     |
287 | 231, 285,
286 | syl2an 480 |
. . . . . . . . . . . . . 14
       
    coeff           |
288 | 284, 287 | syldan 473 |
. . . . . . . . . . . . 13
          coeff           |
289 | 272, 288 | mulcld 9663 |
. . . . . . . . . . . 12
           coeff              coeff            |
290 | 267, 289 | sylan2br 479 |
. . . . . . . . . . 11
             coeff              coeff            |
291 | | id 22 |
. . . . . . . . . . . . . 14
       |
292 | 291, 260 | syl6eqr 2503 |
. . . . . . . . . . . . 13
     |
293 | 292 | fveq2d 5869 |
. . . . . . . . . . . 12
    coeff              coeff               |
294 | 292 | oveq2d 6306 |
. . . . . . . . . . . . 13
             |
295 | 294 | fveq2d 5869 |
. . . . . . . . . . . 12
    coeff          coeff           |
296 | 293, 295 | oveq12d 6308 |
. . . . . . . . . . 11
     coeff              coeff            coeff              coeff            |
297 | 266, 290,
296 | fsump1 13817 |
. . . . . . . . . 10
 
           coeff              coeff                   coeff              coeff            coeff              coeff             |
298 | 262, 297 | syl5eq 2497 |
. . . . . . . . 9
 
         coeff              coeff                   coeff              coeff            coeff              coeff             |
299 | | eldifn 3556 |
. . . . . . . . . . . . . 14
            
      |
300 | 299 | adantl 468 |
. . . . . . . . . . . . 13
                
      |
301 | | eldifi 3555 |
. . . . . . . . . . . . . . . . 17
                
    |
302 | | elfznn0 11887 |
. . . . . . . . . . . . . . . . 17
         |
303 | 301, 302 | syl 17 |
. . . . . . . . . . . . . . . 16
               |
304 | 176, 169 | dgrub 23188 |
. . . . . . . . . . . . . . . . 17
          Poly   coeff             
deg            |
305 | 304 | 3expia 1210 |
. . . . . . . . . . . . . . . 16
          Poly     coeff            
deg             |
306 | 69, 303, 305 | syl2an 480 |
. . . . . . . . . . . . . . 15
                
  coeff            
deg             |
307 | | elfzuz 11796 |
. . . . . . . . . . . . . . . . . . 19
             |
308 | 301, 307 | syl 17 |
. . . . . . . . . . . . . . . . . 18
                   |
309 | 308 | adantl 468 |
. . . . . . . . . . . . . . . . 17
                
      |
310 | | 1z 10967 |
. . . . . . . . . . . . . . . . 17
 |
311 | | elfz5 11792 |
. . . . . . . . . . . . . . . . 17
           
   |
312 | 309, 310,
311 | sylancl 668 |
. . . . . . . . . . . . . . . 16
                
        |
313 | 161 | breq2d 4414 |
. . . . . . . . . . . . . . . . 17
 
 
deg         
   |
314 | 313 | adantr 467 |
. . . . . . . . . . . . . . . 16
                
 deg         
   |
315 | 312, 314 | bitr4d 260 |
. . . . . . . . . . . . . . 15
                
     deg             |
316 | 306, 315 | sylibrd 238 |
. . . . . . . . . . . . . 14
                
  coeff                    |
317 | 316 | necon1bd 2642 |
. . . . . . . . . . . . 13
                

     coeff                |
318 | 300, 317 | mpd 15 |
. . . . . . . . . . . 12
                
 coeff               |
319 | 318 | oveq1d 6305 |
. . . . . . . . . . 11
                
  coeff              coeff            coeff            |
320 | 301, 287 | sylan2 477 |
. . . . . . . . . . . 12
                
 coeff           |
321 | 320 | mul02d 9831 |
. . . . . . . . . . 11
                
  coeff            |
322 | 319, 321 | eqtrd 2485 |
. . . . . . . . . 10
                
  coeff              coeff            |
323 | | fzfid 12186 |
. . . . . . . . . 10
 
         |
324 | 283, 289,
322, 323 | fsumss 13791 |
. . . . . . . . 9
 
         coeff              coeff                    coeff              coeff            |
325 | | 0z 10948 |
. . . . . . . . . . . 12
 |
326 | 189 | fveq1d 5867 |
. . . . . . . . . . . . . . 15
 
  coeff               coeff    coeff            |
327 | | coeidp 23217 |
. . . . . . . . . . . . . . . . . . . 20

 coeff             |
328 | 162 | nesymi 2681 |
. . . . . . . . . . . . . . . . . . . . 21
 |
329 | 328 | iffalsei 3891 |
. . . . . . . . . . . . . . . . . . . 20
      |
330 | 327, 329 | syl6eq 2501 |
. . . . . . . . . . . . . . . . . . 19

 coeff        |
331 | 330 | adantl 468 |
. . . . . . . . . . . . . . . . . 18
      coeff        |
332 | | 0cn 9635 |
. . . . . . . . . . . . . . . . . . . . 21
 |
333 | | vex 3048 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
334 | 333 | fvconst2 6120 |
. . . . . . . . . . . . . . . . . . . . 21
           |
335 | 332, 334 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
         |
336 | 187 | coefv0 23202 |
. . . . . . . . . . . . . . . . . . . . 21
     Poly           coeff           |
337 | 185, 336 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
 
          coeff           |
338 | 335, 337 | syl5reqr 2500 |
. . . . . . . . . . . . . . . . . . 19
 
  coeff           |
339 | 338 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
      coeff           |
340 | 195, 198,
200, 200, 201, 331, 339 | ofval 6540 |
. . . . . . . . . . . . . . . . 17
       coeff    coeff              |
341 | 263, 340 | mpan2 677 |
. . . . . . . . . . . . . . . 16
 
   coeff    coeff              |
342 | | df-neg 9863 |
. . . . . . . . . . . . . . . 16
    |
343 | 341, 342 | syl6eqr 2503 |
. . . . . . . . . . . . . . 15
 
   coeff    coeff             |
344 | 326, 343 | eqtrd 2485 |
. . . . . . . . . . . . . 14
 
  coeff                |
345 | 277 | oveq1d 6305 |
. . . . . . . . . . . . . . . . 17
 
         |
346 | 103 | subid1d 9975 |
. . . . . . . . . . . . . . . . 17
 
 
   |
347 | 345, 346,
31 | 3eqtrd 2489 |
. . . . . . . . . . . . . . . 16
 
     deg    |
348 | 347 | fveq2d 5869 |
. . . . . . . . . . . . . . 15
 
  coeff          coeff    deg     |
349 | 348, 235 | eqtr4d 2488 |
. . . . . . . . . . . . . 14
 
  coeff               |
350 | 344, 349 | oveq12d 6308 |
. . . . . . . . . . . . 13
 
   coeff              coeff                   |
351 | 350, 252 | eqeltrd 2529 |
. . . . . . . . . . . 12
 
   coeff              coeff            |
352 | | fveq2 5865 |
. . . . . . . . . . . . . 14
  coeff              coeff               |
353 | | oveq2 6298 |
. . . . . . . . . . . . . . 15
           |
354 | 353 | fveq2d 5869 |
. . . . . . . . . . . . . 14
  coeff          coeff           |
355 | 352, 354 | oveq12d 6308 |
. . . . . . . . . . . . 13
   coeff              coeff            coeff              coeff            |
356 | 355 | fsum1 13808 |
. . . . . . . . . . . 12
    coeff              coeff                   coeff              coeff            coeff              coeff            |
357 | 325, 351,
356 | sylancr 669 |
. . . . . . . . . . 11
 
         coeff              coeff            coeff              coeff            |
358 | 357, 350 | eqtrd 2485 |
. . . . . . . . . 10
 
         coeff              coeff                   |
359 | 277 | oveq1d 6305 |
. . . . . . . . . . . . 13
 
         |
360 | 359 | fveq2d 5869 |
. . . . . . . . . . . 12
 
  coeff          coeff         |
361 | 227, 360 | oveq12d 6308 |
. . . . . . . . . . 11
 
   coeff              coeff            coeff    
     |
362 | 244 | mulid2d 9661 |
. . . . . . . . . . 11
 
   coeff    
    coeff         |
363 | 361, 362 | eqtrd 2485 |
. . . . . . . . . 10
 
   coeff              coeff           coeff         |
364 | 358, 363 | oveq12d 6308 |
. . . . . . . . 9
 
          coeff              coeff            coeff              coeff                    coeff          |
365 | 298, 324,
364 | 3eqtr3rd 2494 |
. . . . . . . 8
 
          coeff    
   
         coeff              coeff            |
366 | 258, 259,
365 | 3eqtr4rd 2496 |
. . . . . . 7
 
          coeff    
           |
367 | 366 | oveq1d 6305 |
. . . . . 6
 
           coeff                 
         |
368 | 240, 245,
249 | divcan4d 10389 |
. . . . . . 7
 
                 |
369 | 368 | oveq1d 6305 |
. . . . . 6
 
                 coeff                 coeff               |
370 | 253, 367,
369 | 3eqtr3rd 2494 |
. . . . 5
 
     coeff                 
         |
371 | 370 | negeqd 9869 |
. . . 4
 
      coeff                  
         |
372 | 251, 371 | eqtr3d 2487 |
. . 3
 
   
   coeff                            |
373 | 129, 239,
372 | 3eqtrd 2489 |
. 2
 
 
     
         |
374 | 25, 373 | exlimddv 1781 |
1
 
               |