Step | Hyp | Ref
| Expression |
1 | | elaa2lemOLD.f |
. . . 4
      deg                 |
2 | 1 | a1i 11 |
. . 3
       deg                  |
3 | | zsscn 10952 |
. . . . 5
 |
4 | 3 | a1i 11 |
. . . 4

  |
5 | | elaa2lemOLD.g |
. . . . . . . . 9
 Poly    |
6 | | dgrcl 23199 |
. . . . . . . . 9
 Poly  deg    |
7 | 5, 6 | syl 17 |
. . . . . . . 8
 deg    |
8 | 7 | nn0zd 11045 |
. . . . . . 7
 deg    |
9 | | elaa2lemOLD.m |
. . . . . . . . 9
    coeff         |
10 | | ssrab2 3516 |
. . . . . . . . . 10
  coeff       |
11 | | nn0uz 11200 |
. . . . . . . . . . . . 13
     |
12 | 10, 11 | sseqtri 3466 |
. . . . . . . . . . . 12
  coeff           |
13 | 12 | a1i 11 |
. . . . . . . . . . 11
   coeff            |
14 | | elaa2lemOLD.gn0 |
. . . . . . . . . . . . . . . . 17
    |
15 | 14 | neneqd 2631 |
. . . . . . . . . . . . . . . 16
    |
16 | | eqid 2453 |
. . . . . . . . . . . . . . . . . 18
deg  deg   |
17 | | eqid 2453 |
. . . . . . . . . . . . . . . . . 18
coeff  coeff   |
18 | 16, 17 | dgreq0 23231 |
. . . . . . . . . . . . . . . . 17
 Poly   
 coeff    deg      |
19 | 5, 18 | syl 17 |
. . . . . . . . . . . . . . . 16
    coeff    deg      |
20 | 15, 19 | mtbid 302 |
. . . . . . . . . . . . . . 15
  coeff    deg     |
21 | 20 | neqned 2633 |
. . . . . . . . . . . . . 14
  coeff    deg     |
22 | 7, 21 | jca 535 |
. . . . . . . . . . . . 13
  deg   coeff    deg      |
23 | | fveq2 5870 |
. . . . . . . . . . . . . . 15
 deg 
 coeff      coeff    deg     |
24 | 23 | neeq1d 2685 |
. . . . . . . . . . . . . 14
 deg 
  coeff      coeff    deg      |
25 | 24 | elrab 3198 |
. . . . . . . . . . . . 13
 deg    coeff     
 deg   coeff    deg      |
26 | 22, 25 | sylibr 216 |
. . . . . . . . . . . 12
 deg    coeff        |
27 | | ne0i 3739 |
. . . . . . . . . . . 12
 deg    coeff        coeff        |
28 | 26, 27 | syl 17 |
. . . . . . . . . . 11
   coeff        |
29 | | infmssuzclOLD 11254 |
. . . . . . . . . . 11
    coeff            coeff         
 coeff          coeff        |
30 | 13, 28, 29 | syl2anc 667 |
. . . . . . . . . 10
     coeff          coeff        |
31 | 10, 30 | sseldi 3432 |
. . . . . . . . 9
     coeff          |
32 | 9, 31 | syl5eqel 2535 |
. . . . . . . 8
   |
33 | 32 | nn0zd 11045 |
. . . . . . 7
   |
34 | 8, 33 | zsubcld 11052 |
. . . . . 6
  deg     |
35 | 9 | a1i 11 |
. . . . . . . 8
   
 coeff       
  |
36 | | infmssuzleOLD 11253 |
. . . . . . . . 9
    coeff          deg    coeff         
 coeff       
deg    |
37 | 13, 26, 36 | syl2anc 667 |
. . . . . . . 8
     coeff       
deg    |
38 | 35, 37 | eqbrtrd 4426 |
. . . . . . 7

deg    |
39 | 7 | nn0red 10933 |
. . . . . . . 8
 deg    |
40 | 32 | nn0red 10933 |
. . . . . . . 8
   |
41 | 39, 40 | subge0d 10210 |
. . . . . . 7
   deg  
deg     |
42 | 38, 41 | mpbird 236 |
. . . . . 6

 deg     |
43 | 34, 42 | jca 535 |
. . . . 5
   deg    deg      |
44 | | elnn0z 10957 |
. . . . 5
  deg     deg    deg      |
45 | 43, 44 | sylibr 216 |
. . . 4
  deg     |
46 | | id 22 |
. . . . . . . . 9
 Poly  Poly    |
47 | | 0zd 10956 |
. . . . . . . . 9
 Poly    |
48 | 17 | coef2 23197 |
. . . . . . . . 9
  Poly 
 coeff        |
49 | 46, 47, 48 | syl2anc 667 |
. . . . . . . 8
 Poly  coeff        |
50 | 5, 49 | syl 17 |
. . . . . . 7
 coeff        |
51 | 50 | adantr 467 |
. . . . . 6
 

coeff        |
52 | | simpr 463 |
. . . . . . 7
 

  |
53 | 32 | adantr 467 |
. . . . . . 7
 

  |
54 | 52, 53 | nn0addcld 10936 |
. . . . . 6
 

    |
55 | 51, 54 | ffvelrnd 6028 |
. . . . 5
 

 coeff         |
56 | | elaa2lemOLD.i |
. . . . 5
  coeff         |
57 | 55, 56 | fmptd 6051 |
. . . 4
       |
58 | | elplyr 23167 |
. . . 4
 
 deg              deg                Poly    |
59 | 4, 45, 57, 58 | syl3anc 1269 |
. . 3
       deg                Poly    |
60 | 2, 59 | eqeltrd 2531 |
. 2
 Poly    |
61 | | simpr 463 |
. . . . . . . . . 10
     deg   
 deg     |
62 | 61 | iftrued 3891 |
. . . . . . . . 9
     deg   
 
 deg     coeff          coeff         |
63 | | iffalse 3892 |
. . . . . . . . . . 11

 deg  
 
 deg     coeff           |
64 | 63 | adantl 468 |
. . . . . . . . . 10
     deg       deg     coeff           |
65 | | simpr 463 |
. . . . . . . . . . . . . . 15
     deg     deg     |
66 | 39 | ad2antrr 733 |
. . . . . . . . . . . . . . . . 17
     deg    deg    |
67 | 40 | ad2antrr 733 |
. . . . . . . . . . . . . . . . 17
     deg      |
68 | 66, 67 | resubcld 10054 |
. . . . . . . . . . . . . . . 16
     deg     deg     |
69 | | nn0re 10885 |
. . . . . . . . . . . . . . . . 17

  |
70 | 69 | ad2antlr 734 |
. . . . . . . . . . . . . . . 16
     deg      |
71 | 68, 70 | ltnled 9787 |
. . . . . . . . . . . . . . 15
     deg      deg  
 deg      |
72 | 65, 71 | mpbird 236 |
. . . . . . . . . . . . . 14
     deg     deg     |
73 | 66, 67, 70 | ltsubaddd 10216 |
. . . . . . . . . . . . . 14
     deg      deg  
deg 
     |
74 | 72, 73 | mpbid 214 |
. . . . . . . . . . . . 13
     deg    deg      |
75 | | olc 386 |
. . . . . . . . . . . . 13
 deg   
  deg       |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . 12
     deg    
 deg       |
77 | 5 | ad2antrr 733 |
. . . . . . . . . . . . 13
     deg    Poly    |
78 | 54 | adantr 467 |
. . . . . . . . . . . . 13
     deg        |
79 | 16, 17 | dgrlt 23232 |
. . . . . . . . . . . . 13
  Poly 
      deg      deg     coeff           |
80 | 77, 78, 79 | syl2anc 667 |
. . . . . . . . . . . 12
     deg       deg      deg     coeff           |
81 | 76, 80 | mpbid 214 |
. . . . . . . . . . 11
     deg     deg   
 coeff          |
82 | 81 | simprd 465 |
. . . . . . . . . 10
     deg     coeff         |
83 | 64, 82 | eqtr4d 2490 |
. . . . . . . . 9
     deg       deg     coeff          coeff         |
84 | 62, 83 | pm2.61dan 801 |
. . . . . . . 8
 

 
 deg     coeff          coeff         |
85 | 84 | mpteq2dva 4492 |
. . . . . . 7
     deg     coeff            coeff          |
86 | 50, 4 | fssd 5743 |
. . . . . . . . . 10
 coeff        |
87 | 86 | adantr 467 |
. . . . . . . . 9
 
    deg     coeff        |
88 | | elfznn0 11894 |
. . . . . . . . . . 11
     deg   
  |
89 | 88 | adantl 468 |
. . . . . . . . . 10
 
    deg       |
90 | 32 | adantr 467 |
. . . . . . . . . 10
 
    deg       |
91 | 89, 90 | nn0addcld 10936 |
. . . . . . . . 9
 
    deg         |
92 | 87, 91 | ffvelrnd 6028 |
. . . . . . . 8
 
    deg      coeff         |
93 | | eqidd 2454 |
. . . . . . . . . . 11
 

    deg        deg      |
94 | | simpl 459 |
. . . . . . . . . . . . . 14
 
    deg       |
95 | 56 | a1i 11 |
. . . . . . . . . . . . . . 15
 
 coeff          |
96 | 95, 55 | fvmpt2d 5964 |
. . . . . . . . . . . . . 14
 

     coeff         |
97 | 94, 89, 96 | syl2anc 667 |
. . . . . . . . . . . . 13
 
    deg          coeff         |
98 | 97 | adantlr 722 |
. . . . . . . . . . . 12
        deg          coeff         |
99 | 98 | oveq1d 6310 |
. . . . . . . . . . 11
        deg                 coeff              |
100 | 93, 99 | sumeq12rdv 13785 |
. . . . . . . . . 10
 

     deg                    deg       coeff              |
101 | 100 | mpteq2dva 4492 |
. . . . . . . . 9
       deg                      deg       coeff               |
102 | 2, 101 | eqtrd 2487 |
. . . . . . . 8
       deg       coeff               |
103 | 60, 45, 92, 102 | coeeq2 23208 |
. . . . . . 7
 coeff      deg     coeff            |
104 | 85, 103, 95 | 3eqtr4d 2497 |
. . . . . 6
 coeff    |
105 | 104 | fveq1d 5872 |
. . . . 5
  coeff           |
106 | | oveq1 6302 |
. . . . . . . . 9
       |
107 | 106 | adantl 468 |
. . . . . . . 8
 
       |
108 | 3, 33 | sseldi 3432 |
. . . . . . . . . 10
   |
109 | 108 | addid2d 9839 |
. . . . . . . . 9
     |
110 | 109 | adantr 467 |
. . . . . . . 8
 
     |
111 | 107, 110 | eqtrd 2487 |
. . . . . . 7
 
     |
112 | 111 | fveq2d 5874 |
. . . . . 6
 
  coeff        coeff       |
113 | | 0nn0 10891 |
. . . . . . 7
 |
114 | 113 | a1i 11 |
. . . . . 6
   |
115 | 50, 32 | ffvelrnd 6028 |
. . . . . 6
  coeff       |
116 | 95, 112, 114, 115 | fvmptd 5959 |
. . . . 5
      coeff       |
117 | | eqidd 2454 |
. . . . 5
  coeff      coeff       |
118 | 105, 116,
117 | 3eqtrd 2491 |
. . . 4
  coeff      coeff       |
119 | 35, 30 | eqeltrd 2531 |
. . . . . 6
   coeff        |
120 | | fveq2 5870 |
. . . . . . . 8
  coeff      coeff       |
121 | 120 | neeq1d 2685 |
. . . . . . 7
   coeff    
 coeff        |
122 | 121 | elrab 3198 |
. . . . . 6
 
 coeff        coeff        |
123 | 119, 122 | sylib 200 |
. . . . 5
   coeff        |
124 | 123 | simprd 465 |
. . . 4
  coeff       |
125 | 118, 124 | eqnetrd 2693 |
. . 3
  coeff       |
126 | 5, 47 | syl 17 |
. . . . . . 7
   |
127 | | aasscn 23283 |
. . . . . . . . . . 11
 |
128 | | elaa2lemOLD.a |
. . . . . . . . . . 11
   |
129 | 127, 128 | sseldi 3432 |
. . . . . . . . . 10
   |
130 | 94, 129 | syl 17 |
. . . . . . . . 9
 
    deg       |
131 | 130, 89 | expcld 12423 |
. . . . . . . 8
 
    deg           |
132 | 92, 131 | mulcld 9668 |
. . . . . . 7
 
    deg       coeff              |
133 | | oveq1 6302 |
. . . . . . . . 9
           |
134 | 133 | fveq2d 5874 |
. . . . . . . 8
    coeff        coeff           |
135 | | oveq2 6303 |
. . . . . . . 8
               |
136 | 134, 135 | oveq12d 6313 |
. . . . . . 7
     coeff              coeff                  |
137 | 33, 126, 34, 132, 136 | fsumshft 13853 |
. . . . . 6
      deg       coeff            
       deg        coeff                  |
138 | 3, 8 | sseldi 3432 |
. . . . . . . . . 10
 deg    |
139 | 138, 108 | npcand 9995 |
. . . . . . . . 9
   deg    deg    |
140 | 109, 139 | oveq12d 6313 |
. . . . . . . 8
        deg        deg     |
141 | 140 | sumeq1d 13779 |
. . . . . . 7
         deg        coeff                    deg      coeff                  |
142 | | elfzelz 11807 |
. . . . . . . . . . . . . 14
    deg     |
143 | 142 | adantl 468 |
. . . . . . . . . . . . 13
 
   deg      |
144 | 3, 143 | sseldi 3432 |
. . . . . . . . . . . 12
 
   deg      |
145 | 108 | adantr 467 |
. . . . . . . . . . . 12
 
   deg      |
146 | 144, 145 | npcand 9995 |
. . . . . . . . . . 11
 
   deg          |
147 | 146 | fveq2d 5874 |
. . . . . . . . . 10
 
   deg     coeff          coeff       |
148 | 147 | oveq1d 6310 |
. . . . . . . . 9
 
   deg      coeff                  coeff              |
149 | 129 | adantr 467 |
. . . . . . . . . . . 12
 
   deg      |
150 | | elaa2lemOLD.an0 |
. . . . . . . . . . . . 13
   |
151 | 150 | adantr 467 |
. . . . . . . . . . . 12
 
   deg      |
152 | 33 | adantr 467 |
. . . . . . . . . . . 12
 
   deg      |
153 | 149, 151,
152, 143 | expsubd 12434 |
. . . . . . . . . . 11
 
   deg                      |
154 | 153 | oveq2d 6311 |
. . . . . . . . . 10
 
   deg      coeff              coeff                  |
155 | 86 | adantr 467 |
. . . . . . . . . . . . 13
 
   deg    coeff        |
156 | | 0red 9649 |
. . . . . . . . . . . . . . . 16
 
   deg      |
157 | 40 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
   deg      |
158 | 143 | zred 11047 |
. . . . . . . . . . . . . . . 16
 
   deg      |
159 | 32 | nn0ge0d 10935 |
. . . . . . . . . . . . . . . . 17

  |
160 | 159 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
   deg      |
161 | | elfzle1 11809 |
. . . . . . . . . . . . . . . . 17
    deg     |
162 | 161 | adantl 468 |
. . . . . . . . . . . . . . . 16
 
   deg      |
163 | 156, 157,
158, 160, 162 | letrd 9797 |
. . . . . . . . . . . . . . 15
 
   deg      |
164 | 143, 163 | jca 535 |
. . . . . . . . . . . . . 14
 
   deg        |
165 | | elnn0z 10957 |
. . . . . . . . . . . . . 14

    |
166 | 164, 165 | sylibr 216 |
. . . . . . . . . . . . 13
 
   deg      |
167 | 155, 166 | ffvelrnd 6028 |
. . . . . . . . . . . 12
 
   deg     coeff       |
168 | 149, 166 | expcld 12423 |
. . . . . . . . . . . 12
 
   deg          |
169 | 129, 32 | expcld 12423 |
. . . . . . . . . . . . 13
       |
170 | 169 | adantr 467 |
. . . . . . . . . . . 12
 
   deg          |
171 | 149, 151,
152 | expne0d 12429 |
. . . . . . . . . . . 12
 
   deg          |
172 | 167, 168,
170, 171 | divassd 10425 |
. . . . . . . . . . 11
 
   deg       coeff                 coeff                  |
173 | 172 | eqcomd 2459 |
. . . . . . . . . 10
 
   deg      coeff                   coeff                 |
174 | 154, 173 | eqtr2d 2488 |
. . . . . . . . 9
 
   deg       coeff                 coeff              |
175 | 148, 174 | eqtr4d 2490 |
. . . . . . . 8
 
   deg      coeff                   coeff                 |
176 | 175 | sumeq2dv 13781 |
. . . . . . 7
     deg      coeff                    deg       coeff                 |
177 | 141, 176 | eqtrd 2487 |
. . . . . 6
         deg        coeff                    deg       coeff                 |
178 | 32, 11 | syl6eleq 2541 |
. . . . . . . 8
       |
179 | | fzss1 11844 |
. . . . . . . 8
    
   deg  
   deg     |
180 | 178, 179 | syl 17 |
. . . . . . 7
    deg      deg     |
181 | 167, 168 | mulcld 9668 |
. . . . . . . 8
 
   deg      coeff            |
182 | 181, 170,
171 | divcld 10390 |
. . . . . . 7
 
   deg       coeff                 |
183 | 33 | ad2antrr 733 |
. . . . . . . . . . . . . . . . 17
       deg  
   deg    
   |
184 | 8 | ad2antrr 733 |
. . . . . . . . . . . . . . . . 17
       deg  
   deg    
 deg    |
185 | | eldifi 3557 |
. . . . . . . . . . . . . . . . . . 19
     deg      deg       deg     |
186 | | elfznn0 11894 |
. . . . . . . . . . . . . . . . . . . 20
    deg  
  |
187 | 186 | nn0zd 11045 |
. . . . . . . . . . . . . . . . . . 19
    deg  
  |
188 | 185, 187 | syl 17 |
. . . . . . . . . . . . . . . . . 18
     deg      deg      |
189 | 188 | ad2antlr 734 |
. . . . . . . . . . . . . . . . 17
       deg  
   deg    
   |
190 | 183, 184,
189 | 3jca 1189 |
. . . . . . . . . . . . . . . 16
       deg  
   deg    
  deg     |
191 | | simpr 463 |
. . . . . . . . . . . . . . . . 17
       deg  
   deg    

  |
192 | 40 | ad2antrr 733 |
. . . . . . . . . . . . . . . . . 18
       deg  
   deg    
   |
193 | 189 | zred 11047 |
. . . . . . . . . . . . . . . . . 18
       deg  
   deg    
   |
194 | 192, 193 | lenltd 9786 |
. . . . . . . . . . . . . . . . 17
       deg  
   deg    
 
   |
195 | 191, 194 | mpbird 236 |
. . . . . . . . . . . . . . . 16
       deg  
   deg    
   |
196 | | elfzle2 11810 |
. . . . . . . . . . . . . . . . . 18
    deg  
deg    |
197 | 185, 196 | syl 17 |
. . . . . . . . . . . . . . . . 17
     deg      deg   
deg    |
198 | 197 | ad2antlr 734 |
. . . . . . . . . . . . . . . 16
       deg  
   deg    
 deg    |
199 | 190, 195,
198 | jca32 538 |
. . . . . . . . . . . . . . 15
       deg  
   deg    
   deg   
deg      |
200 | | elfz2 11798 |
. . . . . . . . . . . . . . 15
    deg     deg   
deg      |
201 | 199, 200 | sylibr 216 |
. . . . . . . . . . . . . 14
       deg  
   deg    
    deg     |
202 | | eldifn 3558 |
. . . . . . . . . . . . . . 15
     deg      deg   
   deg     |
203 | 202 | ad2antlr 734 |
. . . . . . . . . . . . . 14
       deg  
   deg    

   deg     |
204 | 201, 203 | condan 804 |
. . . . . . . . . . . . 13
 
    deg  
   deg    
  |
205 | 204 | adantr 467 |
. . . . . . . . . . . 12
       deg  
   deg      coeff     
  |
206 | 9 | a1i 11 |
. . . . . . . . . . . . . 14
       deg  
   deg      coeff     
  
 coeff       
  |
207 | 12 | a1i 11 |
. . . . . . . . . . . . . . 15
       deg  
   deg      coeff      
 coeff            |
208 | 185, 186 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
     deg      deg      |
209 | 208 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
      deg      deg     coeff        |
210 | | neqne 37384 |
. . . . . . . . . . . . . . . . . . 19
  coeff      coeff       |
211 | 210 | adantl 468 |
. . . . . . . . . . . . . . . . . 18
      deg      deg     coeff       coeff       |
212 | 209, 211 | jca 535 |
. . . . . . . . . . . . . . . . 17
      deg      deg     coeff      
 coeff        |
213 | | fveq2 5870 |
. . . . . . . . . . . . . . . . . . 19
  coeff      coeff       |
214 | 213 | neeq1d 2685 |
. . . . . . . . . . . . . . . . . 18
   coeff    
 coeff        |
215 | 214 | elrab 3198 |
. . . . . . . . . . . . . . . . 17
 
 coeff        coeff        |
216 | 212, 215 | sylibr 216 |
. . . . . . . . . . . . . . . 16
      deg      deg     coeff        coeff        |
217 | 216 | adantll 721 |
. . . . . . . . . . . . . . 15
       deg  
   deg      coeff        coeff        |
218 | | infmssuzleOLD 11253 |
. . . . . . . . . . . . . . 15
    coeff         
  coeff      
  
 coeff       
  |
219 | 207, 217,
218 | syl2anc 667 |
. . . . . . . . . . . . . 14
       deg  
   deg      coeff        
 coeff       
  |
220 | 206, 219 | eqbrtrd 4426 |
. . . . . . . . . . . . 13
       deg  
   deg      coeff        |
221 | 40 | ad2antrr 733 |
. . . . . . . . . . . . . 14
       deg  
   deg      coeff     
  |
222 | 188 | zred 11047 |
. . . . . . . . . . . . . . 15
     deg      deg      |
223 | 222 | ad2antlr 734 |
. . . . . . . . . . . . . 14
       deg  
   deg      coeff        |
224 | 221, 223 | lenltd 9786 |
. . . . . . . . . . . . 13
       deg  
   deg      coeff          |
225 | 220, 224 | mpbid 214 |
. . . . . . . . . . . 12
       deg  
   deg      coeff     
  |
226 | 205, 225 | condan 804 |
. . . . . . . . . . 11
 
    deg  
   deg      coeff       |
227 | 226 | oveq1d 6310 |
. . . . . . . . . 10
 
    deg  
   deg       coeff                  |
228 | 129 | adantr 467 |
. . . . . . . . . . . 12
 
    deg  
   deg    
  |
229 | 208 | adantl 468 |
. . . . . . . . . . . 12
 
    deg  
   deg       |
230 | 228, 229 | expcld 12423 |
. . . . . . . . . . 11
 
    deg  
   deg           |
231 | 230 | mul02d 9836 |
. . . . . . . . . 10
 
    deg  
   deg             |
232 | 227, 231 | eqtrd 2487 |
. . . . . . . . 9
 
    deg  
   deg       coeff            |
233 | 232 | oveq1d 6310 |
. . . . . . . 8
 
    deg  
   deg        coeff                       |
234 | 129, 150,
33 | expne0d 12429 |
. . . . . . . . . 10
       |
235 | 169, 234 | div0d 10389 |
. . . . . . . . 9
         |
236 | 235 | adantr 467 |
. . . . . . . 8
 
    deg  
   deg             |
237 | 233, 236 | eqtrd 2487 |
. . . . . . 7
 
    deg  
   deg        coeff                 |
238 | | fzfid 12193 |
. . . . . . 7
    deg     |
239 | 180, 182,
237, 238 | fsumss 13803 |
. . . . . 6
     deg       coeff                   deg       coeff                 |
240 | 137, 177,
239 | 3eqtrd 2491 |
. . . . 5
      deg       coeff            
   deg       coeff                 |
241 | 89, 55 | syldan 473 |
. . . . . . . . . 10
 
    deg      coeff         |
242 | 56 | fvmpt2 5962 |
. . . . . . . . . 10
   coeff             coeff         |
243 | 89, 241, 242 | syl2anc 667 |
. . . . . . . . 9
 
    deg          coeff         |
244 | 243 | adantlr 722 |
. . . . . . . 8
        deg          coeff         |
245 | | oveq1 6302 |
. . . . . . . . 9
           |
246 | 245 | ad2antlr 734 |
. . . . . . . 8
        deg               |
247 | 244, 246 | oveq12d 6313 |
. . . . . . 7
        deg                 coeff              |
248 | 247 | sumeq2dv 13781 |
. . . . . 6
 
      deg                    deg       coeff              |
249 | | fzfid 12193 |
. . . . . . 7
     deg      |
250 | 249, 132 | fsumcl 13811 |
. . . . . 6
      deg       coeff              |
251 | 2, 248, 129, 250 | fvmptd 5959 |
. . . . 5
          deg       coeff              |
252 | 17, 16 | coeid2 23205 |
. . . . . . . 8
  Poly 
         deg      coeff            |
253 | 5, 129, 252 | syl2anc 667 |
. . . . . . 7
         deg      coeff            |
254 | 253 | oveq1d 6310 |
. . . . . 6
                deg      coeff                 |
255 | 86 | adantr 467 |
. . . . . . . . 9
 
   deg    coeff        |
256 | 186 | adantl 468 |
. . . . . . . . 9
 
   deg      |
257 | 255, 256 | ffvelrnd 6028 |
. . . . . . . 8
 
   deg     coeff       |
258 | 129 | adantr 467 |
. . . . . . . . 9
 
   deg      |
259 | 258, 256 | expcld 12423 |
. . . . . . . 8
 
   deg          |
260 | 257, 259 | mulcld 9668 |
. . . . . . 7
 
   deg      coeff            |
261 | 238, 169,
260, 234 | fsumdivc 13859 |
. . . . . 6
      deg      coeff                   deg       coeff                 |
262 | 254, 261 | eqtrd 2487 |
. . . . 5
               deg       coeff                 |
263 | 240, 251,
262 | 3eqtr4d 2497 |
. . . 4
                 |
264 | | elaa2lemOLD.ga |
. . . . 5
       |
265 | 264 | oveq1d 6310 |
. . . 4
                   |
266 | 263, 265,
235 | 3eqtrd 2491 |
. . 3
       |
267 | 125, 266 | jca 535 |
. 2
   coeff            |
268 | | fveq2 5870 |
. . . . . 6
 coeff  coeff    |
269 | 268 | fveq1d 5872 |
. . . . 5
  coeff      coeff       |
270 | 269 | neeq1d 2685 |
. . . 4
   coeff    
 coeff        |
271 | | fveq1 5869 |
. . . . 5
           |
272 | 271 | eqeq1d 2455 |
. . . 4
             |
273 | 270, 272 | anbi12d 718 |
. . 3
    coeff            coeff             |
274 | 273 | rspcev 3152 |
. 2
  Poly 
  coeff    
       Poly     coeff            |
275 | 60, 267, 274 | syl2anc 667 |
1
  Poly     coeff            |