Step | Hyp | Ref
| Expression |
1 | | elqaa.1 |
. 2
   |
2 | | cnex 9638 |
. . . . . . . 8
 |
3 | 2 | a1i 11 |
. . . . . . 7
   |
4 | | elqaa.6 |
. . . . . . . . 9
     deg    |
5 | | fvex 5889 |
. . . . . . . . 9
     deg    |
6 | 4, 5 | eqeltri 2545 |
. . . . . . . 8
 |
7 | 6 | a1i 11 |
. . . . . . 7
 

  |
8 | | fvex 5889 |
. . . . . . . 8
     |
9 | 8 | a1i 11 |
. . . . . . 7
 

      |
10 | | fconstmpt 4883 |
. . . . . . . 8
       |
11 | 10 | a1i 11 |
. . . . . . 7
         |
12 | | elqaa.2 |
. . . . . . . . . 10
  Poly        |
13 | 12 | eldifad 3402 |
. . . . . . . . 9
 Poly    |
14 | | plyf 23231 |
. . . . . . . . 9
 Poly        |
15 | 13, 14 | syl 17 |
. . . . . . . 8
       |
16 | 15 | feqmptd 5932 |
. . . . . . 7
         |
17 | 3, 7, 9, 11, 16 | offval2 6567 |
. . . . . 6
                  |
18 | | fzfid 12224 |
. . . . . . . . 9
 

   deg     |
19 | | nn0uz 11217 |
. . . . . . . . . . . . . 14
     |
20 | | 0zd 10973 |
. . . . . . . . . . . . . 14
   |
21 | | ssrab2 3500 |
. . . . . . . . . . . . . . 15
         |
22 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
23 | 22 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . . . 21
               |
24 | 23 | eleq1d 2533 |
. . . . . . . . . . . . . . . . . . . 20
       
         |
25 | 24 | rabbidv 3022 |
. . . . . . . . . . . . . . . . . . 19
                   |
26 | 25 | infeq1d 8011 |
. . . . . . . . . . . . . . . . . 18
 inf           inf             |
27 | | elqaa.5 |
. . . . . . . . . . . . . . . . . 18
 inf         
   |
28 | | ltso 9732 |
. . . . . . . . . . . . . . . . . . 19
 |
29 | 28 | infex 8027 |
. . . . . . . . . . . . . . . . . 18
inf            |
30 | 26, 27, 29 | fvmpt 5963 |
. . . . . . . . . . . . . . . . 17

    inf             |
31 | 30 | adantl 473 |
. . . . . . . . . . . . . . . 16
 

    inf 
       
   |
32 | | nnuz 11218 |
. . . . . . . . . . . . . . . . . 18
     |
33 | 21, 32 | sseqtri 3450 |
. . . . . . . . . . . . . . . . 17
             |
34 | | 0z 10972 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
35 | | zq 11293 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
36 | 34, 35 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
 |
37 | | elqaa.4 |
. . . . . . . . . . . . . . . . . . . . . 22
coeff   |
38 | 37 | coef2 23264 |
. . . . . . . . . . . . . . . . . . . . 21
  Poly 
       |
39 | 13, 36, 38 | sylancl 675 |
. . . . . . . . . . . . . . . . . . . 20
       |
40 | 39 | ffvelrnda 6037 |
. . . . . . . . . . . . . . . . . . 19
 

      |
41 | | qmulz 11290 |
. . . . . . . . . . . . . . . . . . 19
              |
42 | 40, 41 | syl 17 |
. . . . . . . . . . . . . . . . . 18
 

         |
43 | | rabn0 3755 |
. . . . . . . . . . . . . . . . . 18
                  |
44 | 42, 43 | sylibr 217 |
. . . . . . . . . . . . . . . . 17
 

          |
45 | | infssuzcl 11268 |
. . . . . . . . . . . . . . . . 17
             
         inf         
           |
46 | 33, 44, 45 | sylancr 676 |
. . . . . . . . . . . . . . . 16
 

inf                     |
47 | 31, 46 | eqeltrd 2549 |
. . . . . . . . . . . . . . 15
 

              |
48 | 21, 47 | sseldi 3416 |
. . . . . . . . . . . . . 14
 

      |
49 | | nnmulcl 10654 |
. . . . . . . . . . . . . . 15
 
     |
50 | 49 | adantl 473 |
. . . . . . . . . . . . . 14
 
       |
51 | 19, 20, 48, 50 | seqf 12272 |
. . . . . . . . . . . . 13
          |
52 | | dgrcl 23266 |
. . . . . . . . . . . . . 14
 Poly  deg    |
53 | 13, 52 | syl 17 |
. . . . . . . . . . . . 13
 deg    |
54 | 51, 53 | ffvelrnd 6038 |
. . . . . . . . . . . 12
      deg     |
55 | 4, 54 | syl5eqel 2553 |
. . . . . . . . . . 11
   |
56 | 55 | nncnd 10647 |
. . . . . . . . . 10
   |
57 | 56 | adantr 472 |
. . . . . . . . 9
 

  |
58 | | elfznn0 11913 |
. . . . . . . . . 10
    deg  
  |
59 | 37 | coef3 23265 |
. . . . . . . . . . . . . 14
 Poly        |
60 | 13, 59 | syl 17 |
. . . . . . . . . . . . 13
       |
61 | 60 | adantr 472 |
. . . . . . . . . . . 12
 

      |
62 | 61 | ffvelrnda 6037 |
. . . . . . . . . . 11
           |
63 | | expcl 12328 |
. . . . . . . . . . . 12
 
       |
64 | 63 | adantll 728 |
. . . . . . . . . . 11
           |
65 | 62, 64 | mulcld 9681 |
. . . . . . . . . 10
                 |
66 | 58, 65 | sylan2 482 |
. . . . . . . . 9
       deg                |
67 | 18, 57, 66 | fsummulc2 13922 |
. . . . . . . 8
 

     deg                   deg                  |
68 | | eqid 2471 |
. . . . . . . . . . 11
deg  deg   |
69 | 37, 68 | coeid2 23272 |
. . . . . . . . . 10
  Poly 
         deg                |
70 | 13, 69 | sylan 479 |
. . . . . . . . 9
 

    
   deg                |
71 | 70 | oveq2d 6324 |
. . . . . . . 8
 

           deg                 |
72 | 57 | adantr 472 |
. . . . . . . . . . 11
       |
73 | 72, 62, 64 | mulassd 9684 |
. . . . . . . . . 10
                               |
74 | 58, 73 | sylan2 482 |
. . . . . . . . 9
       deg                              |
75 | 74 | sumeq2dv 13846 |
. . . . . . . 8
 

    deg                    deg                  |
76 | 67, 71, 75 | 3eqtr4d 2515 |
. . . . . . 7
 

      
   deg                  |
77 | 76 | mpteq2dva 4482 |
. . . . . 6
  
           deg                   |
78 | 17, 77 | eqtrd 2505 |
. . . . 5
             deg                   |
79 | | zsscn 10969 |
. . . . . . 7
 |
80 | 79 | a1i 11 |
. . . . . 6

  |
81 | 56 | adantr 472 |
. . . . . . . . . . 11
 

  |
82 | 48 | nncnd 10647 |
. . . . . . . . . . 11
 

      |
83 | 48 | nnne0d 10676 |
. . . . . . . . . . 11
 

      |
84 | 81, 82, 83 | divcan2d 10407 |
. . . . . . . . . 10
 

              |
85 | 84 | oveq2d 6324 |
. . . . . . . . 9
 

                          |
86 | 60 | ffvelrnda 6037 |
. . . . . . . . . 10
 

      |
87 | 81, 82, 83 | divcld 10405 |
. . . . . . . . . 10
 

        |
88 | 86, 82, 87 | mulassd 9684 |
. . . . . . . . 9
 

                                      |
89 | 81, 86 | mulcomd 9682 |
. . . . . . . . 9
 

              |
90 | 85, 88, 89 | 3eqtr4rd 2516 |
. . . . . . . 8
 

                          |
91 | 58, 90 | sylan2 482 |
. . . . . . 7
 
   deg                              |
92 | | oveq2 6316 |
. . . . . . . . . . . . 13
                       |
93 | 92 | eleq1d 2533 |
. . . . . . . . . . . 12
           
             |
94 | 93 | elrab 3184 |
. . . . . . . . . . 11
            
                  |
95 | 94 | simprbi 471 |
. . . . . . . . . 10
                         |
96 | 47, 95 | syl 17 |
. . . . . . . . 9
 

            |
97 | 58, 96 | sylan2 482 |
. . . . . . . 8
 
   deg                |
98 | | elqaa.3 |
. . . . . . . . . 10
       |
99 | | eqid 2471 |
. . . . . . . . . 10
                       |
100 | 1, 12, 98, 37, 27, 4, 99 | elqaalem2 23352 |
. . . . . . . . 9
 
   deg            |
101 | 55 | adantr 472 |
. . . . . . . . . 10
 
   deg      |
102 | 58, 48 | sylan2 482 |
. . . . . . . . . 10
 
   deg          |
103 | | nnre 10638 |
. . . . . . . . . . 11
   |
104 | | nnrp 11334 |
. . . . . . . . . . 11
           |
105 | | mod0 12136 |
. . . . . . . . . . 11
                       |
106 | 103, 104,
105 | syl2an 485 |
. . . . . . . . . 10
                       |
107 | 101, 102,
106 | syl2anc 673 |
. . . . . . . . 9
 
   deg                    |
108 | 100, 107 | mpbid 215 |
. . . . . . . 8
 
   deg            |
109 | 97, 108 | zmulcld 11069 |
. . . . . . 7
 
   deg                        |
110 | 91, 109 | eqeltrd 2549 |
. . . . . 6
 
   deg            |
111 | 80, 53, 110 | elplyd 23235 |
. . . . 5
      deg                 Poly    |
112 | 78, 111 | eqeltrd 2549 |
. . . 4
        Poly    |
113 | | eldifsn 4088 |
. . . . . . 7
  Poly 
   
 Poly 
    |
114 | 12, 113 | sylib 201 |
. . . . . 6
  Poly      |
115 | 114 | simprd 470 |
. . . . 5
    |
116 | | oveq1 6315 |
. . . . . . 7
                                 |
117 | 15 | ffvelrnda 6037 |
. . . . . . . . . . 11
 

      |
118 | 55 | nnne0d 10676 |
. . . . . . . . . . . 12
   |
119 | 118 | adantr 472 |
. . . . . . . . . . 11
 

  |
120 | 117, 57, 119 | divcan3d 10410 |
. . . . . . . . . 10
 

              |
121 | 120 | mpteq2dva 4482 |
. . . . . . . . 9
                   |
122 | | ovex 6336 |
. . . . . . . . . . 11
       |
123 | 122 | a1i 11 |
. . . . . . . . . 10
 

        |
124 | 3, 123, 7, 17, 11 | offval2 6567 |
. . . . . . . . 9
                           |
125 | 121, 124,
16 | 3eqtr4d 2515 |
. . . . . . . 8
                 |
126 | 56, 118 | div0d 10404 |
. . . . . . . . . 10
     |
127 | 126 | mpteq2dv 4483 |
. . . . . . . . 9
         |
128 | | 0cnd 9654 |
. . . . . . . . . 10
 

  |
129 | | df-0p 22707 |
. . . . . . . . . . . 12

     |
130 | | fconstmpt 4883 |
. . . . . . . . . . . 12
       |
131 | 129, 130 | eqtri 2493 |
. . . . . . . . . . 11

   |
132 | 131 | a1i 11 |
. . . . . . . . . 10
      |
133 | 3, 128, 7, 132, 11 | offval2 6567 |
. . . . . . . . 9
               |
134 | 127, 133,
132 | 3eqtr4d 2515 |
. . . . . . . 8
            |
135 | 125, 134 | eqeq12d 2486 |
. . . . . . 7
                            |
136 | 116, 135 | syl5ib 227 |
. . . . . 6
         
    |
137 | 136 | necon3d 2664 |
. . . . 5
              |
138 | 115, 137 | mpd 15 |
. . . 4
           |
139 | | eldifsn 4088 |
. . . 4
         Poly     
        Poly             |
140 | 112, 138,
139 | sylanbrc 677 |
. . 3
         Poly 
      |
141 | 6 | fconst 5782 |
. . . . . . 7
           |
142 | | ffn 5739 |
. . . . . . 7
                 |
143 | 141, 142 | mp1i 13 |
. . . . . 6
       |
144 | | ffn 5739 |
. . . . . . 7
       |
145 | 15, 144 | syl 17 |
. . . . . 6
   |
146 | | inidm 3632 |
. . . . . 6
   |
147 | 6 | fvconst2 6136 |
. . . . . . 7
           |
148 | 147 | adantl 473 |
. . . . . 6
 

          |
149 | 98 | adantr 472 |
. . . . . 6
 

      |
150 | 143, 145,
3, 3, 146, 148, 149 | ofval 6559 |
. . . . 5
 

               |
151 | 1, 150 | mpdan 681 |
. . . 4
                |
152 | 56 | mul01d 9850 |
. . . 4
     |
153 | 151, 152 | eqtrd 2505 |
. . 3
              |
154 | | fveq1 5878 |
. . . . 5
                         |
155 | 154 | eqeq1d 2473 |
. . . 4
                           |
156 | 155 | rspcev 3136 |
. . 3
          Poly 
                  Poly             |
157 | 140, 153,
156 | syl2anc 673 |
. 2
   Poly             |
158 | | elaa 23348 |
. 2

   Poly              |
159 | 1, 157, 158 | sylanbrc 677 |
1
   |