Step | Hyp | Ref
| Expression |
1 | | simp3 1011 |
. . . . . . . . . 10
   Poly             |
2 | | eldifi 3523 |
. . . . . . . . . . . . . 14
  Poly 
   
Poly    |
3 | 2 | adantr 471 |
. . . . . . . . . . . . 13
   Poly       Poly    |
4 | 3 | 3adant2 1028 |
. . . . . . . . . . . 12
   Poly           Poly    |
5 | | eldifsni 4067 |
. . . . . . . . . . . . . . 15
  Poly 
       |
6 | 5 | adantr 471 |
. . . . . . . . . . . . . 14
   Poly          |
7 | | 0nn0 10874 |
. . . . . . . . . . . . . . . . . 18
 |
8 | | dgrcl 23199 |
. . . . . . . . . . . . . . . . . . 19
 Poly  deg    |
9 | 3, 8 | syl 17 |
. . . . . . . . . . . . . . . . . 18
   Poly       deg    |
10 | | prssi 4097 |
. . . . . . . . . . . . . . . . . 18
  deg     deg     |
11 | 7, 9, 10 | sylancr 674 |
. . . . . . . . . . . . . . . . 17
   Poly         deg     |
12 | | ssrab2 3482 |
. . . . . . . . . . . . . . . . . 18


   deg        coeff        |
13 | 12 | a1i 11 |
. . . . . . . . . . . . . . . . 17
   Poly       
    deg        coeff         |
14 | 11, 13 | unssd 3578 |
. . . . . . . . . . . . . . . 16
   Poly          deg    
   deg        coeff       
  |
15 | | nn0ssre 10863 |
. . . . . . . . . . . . . . . . 17
 |
16 | | ressxr 9671 |
. . . . . . . . . . . . . . . . 17
 |
17 | 15, 16 | sstri 3409 |
. . . . . . . . . . . . . . . 16
 |
18 | 14, 17 | syl6ss 3412 |
. . . . . . . . . . . . . . 15
   Poly          deg    
   deg        coeff       
  |
19 | | fvex 5858 |
. . . . . . . . . . . . . . . . 17
deg   |
20 | 19 | prid2 4050 |
. . . . . . . . . . . . . . . 16
deg    deg    |
21 | | elun1 3569 |
. . . . . . . . . . . . . . . 16
 deg    deg   deg     deg    
   deg        coeff          |
22 | 20, 21 | ax-mp 5 |
. . . . . . . . . . . . . . 15
deg     deg   
    deg        coeff         |
23 | | supxrub 11600 |
. . . . . . . . . . . . . . 15
     deg  
     deg        coeff       
deg     deg   
    deg        coeff         deg       deg    
   deg        coeff            |
24 | 18, 22, 23 | sylancl 673 |
. . . . . . . . . . . . . 14
   Poly       deg 
     deg  
     deg        coeff            |
25 | 18 | adantr 471 |
. . . . . . . . . . . . . . . 16
    Poly     

    deg   
    deg        coeff       
  |
26 | | fveq2 5848 |
. . . . . . . . . . . . . . . . . . . 20
  coeff         coeff            |
27 | | abs0 13359 |
. . . . . . . . . . . . . . . . . . . 20
     |
28 | 26, 27 | syl6eq 2502 |
. . . . . . . . . . . . . . . . . . 19
  coeff         coeff        |
29 | | c0ex 9624 |
. . . . . . . . . . . . . . . . . . . . 21
 |
30 | 29 | prid1 4049 |
. . . . . . . . . . . . . . . . . . . 20
  deg    |
31 | | elun1 3569 |
. . . . . . . . . . . . . . . . . . . 20
   deg      deg   
    deg        coeff          |
32 | 30, 31 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
   deg  
     deg        coeff         |
33 | 28, 32 | syl6eqel 2538 |
. . . . . . . . . . . . . . . . . 18
  coeff         coeff         deg  
     deg        coeff          |
34 | 33 | adantl 472 |
. . . . . . . . . . . . . . . . 17
     Poly         coeff     
    coeff         deg    
   deg        coeff          |
35 | | 0z 10938 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
36 | | eqid 2452 |
. . . . . . . . . . . . . . . . . . . . . . . 24
coeff  coeff   |
37 | 36 | coef2 23197 |
. . . . . . . . . . . . . . . . . . . . . . 23
  Poly 
 coeff        |
38 | 3, 35, 37 | sylancl 673 |
. . . . . . . . . . . . . . . . . . . . . 22
   Poly       coeff        |
39 | 38 | ffvelrnda 6006 |
. . . . . . . . . . . . . . . . . . . . 21
    Poly     

  coeff       |
40 | | nn0abscl 13386 |
. . . . . . . . . . . . . . . . . . . . 21
  coeff         coeff        |
41 | 39, 40 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
    Poly     

     coeff        |
42 | 41 | adantr 471 |
. . . . . . . . . . . . . . . . . . 19
     Poly         coeff     
    coeff        |
43 | | simplr 767 |
. . . . . . . . . . . . . . . . . . . . 21
     Poly         coeff     
  |
44 | 9 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . 21
     Poly         coeff     
deg    |
45 | 3 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . . 22
     Poly         coeff     
Poly    |
46 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . . . 22
     Poly         coeff     
 coeff       |
47 | | eqid 2452 |
. . . . . . . . . . . . . . . . . . . . . . 23
deg  deg   |
48 | 36, 47 | dgrub 23200 |
. . . . . . . . . . . . . . . . . . . . . 22
  Poly 
 coeff      deg    |
49 | 45, 43, 46, 48 | syl3anc 1271 |
. . . . . . . . . . . . . . . . . . . . 21
     Poly         coeff     
deg    |
50 | | elfz2nn0 11876 |
. . . . . . . . . . . . . . . . . . . . 21
    deg   
deg  deg     |
51 | 43, 44, 49, 50 | syl3anbrc 1193 |
. . . . . . . . . . . . . . . . . . . 20
     Poly         coeff     
   deg     |
52 | | eqid 2452 |
. . . . . . . . . . . . . . . . . . . 20
    coeff          coeff       |
53 | | fveq2 5848 |
. . . . . . . . . . . . . . . . . . . . . . 23
  coeff      coeff       |
54 | 53 | fveq2d 5852 |
. . . . . . . . . . . . . . . . . . . . . 22
     coeff          coeff        |
55 | 54 | eqeq2d 2462 |
. . . . . . . . . . . . . . . . . . . . 21
      coeff          coeff     
    coeff          coeff         |
56 | 55 | rspcev 3118 |
. . . . . . . . . . . . . . . . . . . 20
     deg       coeff          coeff       
   deg        coeff          coeff        |
57 | 51, 52, 56 | sylancl 673 |
. . . . . . . . . . . . . . . . . . 19
     Poly         coeff     
    deg        coeff          coeff        |
58 | | eqeq1 2456 |
. . . . . . . . . . . . . . . . . . . . 21
     coeff           coeff     
    coeff          coeff         |
59 | 58 | rexbidv 2873 |
. . . . . . . . . . . . . . . . . . . 20
     coeff           deg        coeff     
    deg        coeff          coeff         |
60 | 59 | elrab 3164 |
. . . . . . . . . . . . . . . . . . 19
     coeff       
   deg        coeff            coeff     
    deg        coeff          coeff         |
61 | 42, 57, 60 | sylanbrc 675 |
. . . . . . . . . . . . . . . . . 18
     Poly         coeff     
    coeff      

   deg        coeff         |
62 | | elun2 3570 |
. . . . . . . . . . . . . . . . . 18
     coeff       
   deg        coeff           coeff         deg  
     deg        coeff          |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . . . . . . 17
     Poly         coeff     
    coeff         deg    
   deg        coeff          |
64 | 34, 63 | pm2.61dane 2711 |
. . . . . . . . . . . . . . . 16
    Poly     

     coeff         deg   
    deg        coeff          |
65 | | supxrub 11600 |
. . . . . . . . . . . . . . . 16
     deg  
     deg        coeff       
    coeff         deg   
    deg        coeff             coeff           deg    
   deg        coeff            |
66 | 25, 64, 65 | syl2anc 671 |
. . . . . . . . . . . . . . 15
    Poly     

     coeff           deg    
   deg        coeff            |
67 | 66 | ralrimiva 2790 |
. . . . . . . . . . . . . 14
   Poly            coeff           deg    
   deg        coeff            |
68 | 6, 24, 67 | 3jca 1189 |
. . . . . . . . . . . . 13
   Poly         deg       deg    
   deg        coeff               coeff           deg    
   deg        coeff             |
69 | 68 | 3adant2 1028 |
. . . . . . . . . . . 12
   Poly             deg       deg    
   deg        coeff               coeff           deg    
   deg        coeff             |
70 | | neeq1 2686 |
. . . . . . . . . . . . . 14
       |
71 | | fveq2 5848 |
. . . . . . . . . . . . . . 15
 deg  deg    |
72 | 71 | breq1d 4384 |
. . . . . . . . . . . . . 14
  deg       deg    
   deg        coeff          deg       deg    
   deg        coeff             |
73 | | fveq2 5848 |
. . . . . . . . . . . . . . . . . 18
 coeff  coeff    |
74 | 73 | fveq1d 5850 |
. . . . . . . . . . . . . . . . 17
  coeff      coeff       |
75 | 74 | fveq2d 5852 |
. . . . . . . . . . . . . . . 16
     coeff          coeff        |
76 | 75 | breq1d 4384 |
. . . . . . . . . . . . . . 15
      coeff           deg    
   deg        coeff              coeff           deg    
   deg        coeff             |
77 | 76 | ralbidv 2810 |
. . . . . . . . . . . . . 14
  
    coeff           deg    
   deg        coeff          
    coeff           deg    
   deg        coeff             |
78 | 70, 72, 77 | 3anbi123d 1343 |
. . . . . . . . . . . . 13
    deg 
     deg  
     deg        coeff               coeff           deg    
   deg        coeff             deg       deg    
   deg        coeff               coeff           deg    
   deg        coeff              |
79 | 78 | elrab 3164 |
. . . . . . . . . . . 12
  Poly    deg       deg    
   deg        coeff               coeff           deg    
   deg        coeff           
 Poly    deg 
     deg  
     deg        coeff               coeff           deg    
   deg        coeff              |
80 | 4, 69, 79 | sylanbrc 675 |
. . . . . . . . . . 11
   Poly            Poly 
  deg 
     deg  
     deg        coeff               coeff           deg    
   deg        coeff              |
81 | | simp2 1010 |
. . . . . . . . . . 11
   Poly                 |
82 | | fveq1 5847 |
. . . . . . . . . . . . 13
           |
83 | 82 | eqeq1d 2454 |
. . . . . . . . . . . 12
             |
84 | 83 | rspcev 3118 |
. . . . . . . . . . 11
   Poly 
  deg       deg    
   deg        coeff               coeff           deg    
   deg        coeff                 
 Poly 
  deg       deg    
   deg        coeff               coeff           deg    
   deg        coeff                  |
85 | 80, 81, 84 | syl2anc 671 |
. . . . . . . . . 10
   Poly             Poly 
  deg 
     deg  
     deg        coeff               coeff           deg    
   deg        coeff                  |
86 | | fveq2 5848 |
. . . . . . . . . . . . 13
           |
87 | 86 | eqeq1d 2454 |
. . . . . . . . . . . 12
             |
88 | 87 | rexbidv 2873 |
. . . . . . . . . . 11
  
 Poly 
  deg       deg    
   deg        coeff               coeff           deg    
   deg        coeff                  Poly 
  deg 
     deg  
     deg        coeff               coeff           deg    
   deg        coeff                   |
89 | 88 | elrab 3164 |
. . . . . . . . . 10
    Poly    deg 
     deg  
     deg        coeff               coeff           deg    
   deg        coeff                
   Poly    deg 
     deg  
     deg        coeff               coeff           deg    
   deg        coeff                   |
90 | 1, 85, 89 | sylanbrc 675 |
. . . . . . . . 9
   Poly            
 Poly 
  deg       deg    
   deg        coeff               coeff           deg    
   deg        coeff                   |
91 | | prfi 7833 |
. . . . . . . . . . . . . . 15
  deg    |
92 | | fzfi 12179 |
. . . . . . . . . . . . . . . . 17
   deg    |
93 | | abrexfi 7861 |
. . . . . . . . . . . . . . . . 17
    deg        deg        coeff         |
94 | 92, 93 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
     deg        coeff        |
95 | | rabssab 3484 |
. . . . . . . . . . . . . . . 16


   deg        coeff            deg        coeff        |
96 | | ssfi 7779 |
. . . . . . . . . . . . . . . 16
   
   deg        coeff        
   deg        coeff            deg        coeff       
     deg        coeff         |
97 | 94, 95, 96 | mp2an 683 |
. . . . . . . . . . . . . . 15


   deg        coeff        |
98 | | unfi 7825 |
. . . . . . . . . . . . . . 15
    deg    
   deg        coeff           deg  
     deg        coeff          |
99 | 91, 97, 98 | mp2an 683 |
. . . . . . . . . . . . . 14
   deg    
   deg        coeff         |
100 | 99 | a1i 11 |
. . . . . . . . . . . . 13
   Poly          deg    
   deg        coeff          |
101 | 22 | ne0ii 3706 |
. . . . . . . . . . . . . 14
   deg    
   deg        coeff         |
102 | 101 | a1i 11 |
. . . . . . . . . . . . 13
   Poly          deg    
   deg        coeff          |
103 | | xrltso 11430 |
. . . . . . . . . . . . . 14
 |
104 | | fisupcl 7972 |
. . . . . . . . . . . . . 14
     deg  
     deg        coeff           deg   
    deg        coeff           deg   
    deg        coeff       
       deg    
   deg        coeff             deg    
   deg        coeff          |
105 | 103, 104 | mpan 681 |
. . . . . . . . . . . . 13
     deg  
     deg        coeff           deg   
    deg        coeff           deg   
    deg        coeff       
      deg    
   deg        coeff             deg    
   deg        coeff          |
106 | 100, 102,
18, 105 | syl3anc 1271 |
. . . . . . . . . . . 12
   Poly            deg    
   deg        coeff             deg    
   deg        coeff          |
107 | 14, 106 | sseldd 3401 |
. . . . . . . . . . 11
   Poly            deg    
   deg        coeff            |
108 | 107 | 3adant2 1028 |
. . . . . . . . . 10
   Poly                deg    
   deg        coeff            |
109 | | eqidd 2453 |
. . . . . . . . . 10
   Poly              Poly    deg 
     deg  
     deg        coeff               coeff           deg    
   deg        coeff                  
 Poly 
  deg       deg    
   deg        coeff               coeff           deg    
   deg        coeff                   |
110 | | breq2 4378 |
. . . . . . . . . . . . . . . 16
      deg   
    deg        coeff           deg  deg       deg    
   deg        coeff             |
111 | | breq2 4378 |
. . . . . . . . . . . . . . . . 17
      deg   
    deg        coeff               coeff     
    coeff     
     deg  
     deg        coeff             |
112 | 111 | ralbidv 2810 |
. . . . . . . . . . . . . . . 16
      deg   
    deg        coeff                coeff           coeff           deg    
   deg        coeff             |
113 | 110, 112 | 3anbi23d 1346 |
. . . . . . . . . . . . . . 15
      deg   
    deg        coeff             deg 
     coeff      
  deg       deg    
   deg        coeff               coeff           deg    
   deg        coeff              |
114 | 113 | rabbidv 3004 |
. . . . . . . . . . . . . 14
      deg   
    deg        coeff           Poly    deg       coeff         Poly 
  deg 
     deg  
     deg        coeff               coeff           deg    
   deg        coeff              |
115 | 114 | rexeqdv 2962 |
. . . . . . . . . . . . 13
      deg   
    deg        coeff             Poly    deg 
     coeff              Poly 
  deg 
     deg  
     deg        coeff               coeff           deg    
   deg        coeff                   |
116 | 115 | rabbidv 3004 |
. . . . . . . . . . . 12
      deg   
    deg        coeff             Poly    deg 
     coeff              
 Poly 
  deg       deg    
   deg        coeff               coeff           deg    
   deg        coeff                   |
117 | 116 | eqeq2d 2462 |
. . . . . . . . . . 11
      deg   
    deg        coeff            
 Poly    deg       deg    
   deg        coeff               coeff           deg    
   deg        coeff                  
 Poly 
  deg       coeff            
   Poly    deg 
     deg  
     deg        coeff               coeff           deg    
   deg        coeff                  
 Poly 
  deg       deg    
   deg        coeff               coeff           deg    
   deg        coeff                    |
118 | 117 | rspcev 3118 |
. . . . . . . . . 10
       deg    
   deg        coeff         
 
 Poly    deg       deg    
   deg        coeff               coeff           deg    
   deg        coeff                  
 Poly 
  deg       deg    
   deg        coeff               coeff           deg    
   deg        coeff                  
 
 Poly 
  deg       deg    
   deg        coeff               coeff           deg    
   deg        coeff                  
 Poly 
  deg       coeff               |
119 | 108, 109,
118 | syl2anc 671 |
. . . . . . . . 9
   Poly             
 Poly 
  deg       deg    
   deg        coeff               coeff           deg    
   deg        coeff                  
 Poly 
  deg       coeff               |
120 | | cnex 9607 |
. . . . . . . . . . 11
 |
121 | 120 | rabex 4527 |
. . . . . . . . . 10
 
 Poly    deg       deg    
   deg        coeff               coeff           deg    
   deg        coeff                  |
122 | | eleq2 2519 |
. . . . . . . . . . 11
    Poly    deg 
     deg  
     deg        coeff               coeff           deg    
   deg        coeff                 
 
 Poly 
  deg       deg    
   deg        coeff               coeff           deg    
   deg        coeff                    |
123 | | eqeq1 2456 |
. . . . . . . . . . . 12
    Poly    deg 
     deg  
     deg        coeff               coeff           deg    
   deg        coeff                   
 Poly    deg       coeff            
   Poly    deg 
     deg  
     deg        coeff               coeff           deg    
   deg        coeff                  
 Poly 
  deg       coeff                |
124 | 123 | rexbidv 2873 |
. . . . . . . . . . 11
    Poly    deg 
     deg  
     deg        coeff               coeff           deg    
   deg        coeff                  
   Poly    deg 
     coeff            
    Poly    deg 
     deg  
     deg        coeff               coeff           deg    
   deg        coeff                  
 Poly 
  deg       coeff                |
125 | 122, 124 | anbi12d 722 |
. . . . . . . . . 10
    Poly    deg 
     deg  
     deg        coeff               coeff           deg    
   deg        coeff                     
 Poly 
  deg       coeff             
    Poly 
  deg 
     deg  
     deg        coeff               coeff           deg    
   deg        coeff                 
 
 Poly    deg       deg    
   deg        coeff               coeff           deg    
   deg        coeff                  
 Poly 
  deg       coeff                 |
126 | 121, 125 | spcev 3109 |
. . . . . . . . 9
   
 Poly    deg       deg    
   deg        coeff               coeff           deg    
   deg        coeff                 
 
 Poly    deg       deg    
   deg        coeff               coeff           deg    
   deg        coeff                  
 Poly 
  deg       coeff                   
 Poly 
  deg       coeff                |
127 | 90, 119, 126 | syl2anc 671 |
. . . . . . . 8
   Poly              
   Poly 
  deg 
     coeff                |
128 | 127 | 3exp 1209 |
. . . . . . 7
  Poly 
         
     
 Poly 
  deg       coeff                  |
129 | 128 | rexlimiv 2848 |
. . . . . 6
   Poly               
   Poly 
  deg 
     coeff                 |
130 | 129 | impcom 436 |
. . . . 5
    Poly               
   Poly 
  deg 
     coeff                |
131 | | eleq2 2519 |
. . . . . . . . 9
    Poly    deg 
     coeff             
 
 Poly 
  deg       coeff                |
132 | 87 | rexbidv 2873 |
. . . . . . . . . . 11
  
 Poly 
  deg       coeff              Poly 
  deg 
     coeff               |
133 | 132 | elrab 3164 |
. . . . . . . . . 10
    Poly    deg 
     coeff            
   Poly    deg 
     coeff               |
134 | | simp1 1009 |
. . . . . . . . . . . . . . 15
   deg 
     coeff      
   |
135 | 134 | anim2i 577 |
. . . . . . . . . . . . . 14
  Poly 
  deg 
     coeff         Poly 
    |
136 | 71 | breq1d 4384 |
. . . . . . . . . . . . . . . 16
  deg  deg     |
137 | 75 | breq1d 4384 |
. . . . . . . . . . . . . . . . 17
      coeff          coeff         |
138 | 137 | ralbidv 2810 |
. . . . . . . . . . . . . . . 16
  
    coeff           coeff         |
139 | 70, 136, 138 | 3anbi123d 1343 |
. . . . . . . . . . . . . . 15
    deg 
     coeff         deg       coeff          |
140 | 139 | elrab 3164 |
. . . . . . . . . . . . . 14
  Poly    deg       coeff       
 Poly    deg 
     coeff          |
141 | | eldifsn 4066 |
. . . . . . . . . . . . . 14
  Poly 
   
 Poly 
    |
142 | 135, 140,
141 | 3imtr4i 274 |
. . . . . . . . . . . . 13
  Poly    deg       coeff         Poly        |
143 | 142 | ssriv 3404 |
. . . . . . . . . . . 12
 Poly 
  deg       coeff         Poly       |
144 | | ssrexv 3462 |
. . . . . . . . . . . . 13
  Poly 
  deg 
     coeff         Poly     
 
 Poly    deg       coeff           
  Poly              |
145 | 83 | cbvrexv 2988 |
. . . . . . . . . . . . 13
   Poly           
 Poly             |
146 | 144, 145 | syl6ib 234 |
. . . . . . . . . . . 12
  Poly 
  deg 
     coeff         Poly     
 
 Poly    deg       coeff           
  Poly              |
147 | 143, 146 | ax-mp 5 |
. . . . . . . . . . 11
   Poly 
  deg       coeff           
  Poly             |
148 | 147 | anim2i 577 |
. . . . . . . . . 10
    Poly 
  deg       coeff                Poly              |
149 | 133, 148 | sylbi 200 |
. . . . . . . . 9
    Poly    deg 
     coeff                Poly              |
150 | 131, 149 | syl6bi 236 |
. . . . . . . 8
    Poly    deg 
     coeff                 Poly               |
151 | 150 | rexlimivw 2850 |
. . . . . . 7
     Poly 
  deg 
     coeff                 Poly               |
152 | 151 | impcom 436 |
. . . . . 6
      Poly 
  deg 
     coeff                 Poly              |
153 | 152 | exlimiv 1780 |
. . . . 5
      
 Poly 
  deg       coeff                 Poly              |
154 | 130, 153 | impbii 192 |
. . . 4
    Poly                 
 Poly 
  deg       coeff                |
155 | | elaa 23281 |
. . . 4

   Poly              |
156 | | eluniab 4179 |
. . . 4
     
 Poly 
  deg       coeff             
     
 Poly 
  deg       coeff                |
157 | 154, 155,
156 | 3bitr4i 285 |
. . 3

  
   Poly 
  deg 
     coeff                |
158 | 157 | eqriv 2449 |
. 2
  
   Poly 
  deg 
     coeff               |
159 | | aannenlem.a |
. . . 4
    Poly 
  deg 
     coeff               |
160 | 159 | rnmpt 5058 |
. . 3
 
   Poly 
  deg 
     coeff               |
161 | 160 | unieqi 4177 |
. 2
     
 Poly 
  deg       coeff               |
162 | 158, 161 | eqtr4i 2477 |
1
  |