| Step | Hyp | Ref
| Expression |
| 1 | | plycolemc.n |
. 2
   |
| 2 | | oveq2 5930 |
. . . . . . 7
           |
| 3 | 2 | sumeq1d 11531 |
. . . . . 6
                     
                     |
| 4 | 3 | mpteq2dv 4124 |
. . . . 5
                                               |
| 5 | 4 | eleq1d 2265 |
. . . 4
                        Poly 
                      Poly     |
| 6 | 5 | imbi2d 230 |
. . 3
  
                      Poly                          Poly      |
| 7 | | oveq2 5930 |
. . . . . . 7
           |
| 8 | 7 | sumeq1d 11531 |
. . . . . 6
                     
                     |
| 9 | 8 | mpteq2dv 4124 |
. . . . 5
                                               |
| 10 | 9 | eleq1d 2265 |
. . . 4
                        Poly 
                      Poly     |
| 11 | 10 | imbi2d 230 |
. . 3
  
                      Poly                          Poly      |
| 12 | | oveq2 5930 |
. . . . . . 7
               |
| 13 | 12 | sumeq1d 11531 |
. . . . . 6
                       
                       |
| 14 | 13 | mpteq2dv 4124 |
. . . . 5
                                                   |
| 15 | 14 | eleq1d 2265 |
. . . 4
                          Poly 
                        Poly     |
| 16 | 15 | imbi2d 230 |
. . 3
    
                      Poly                            Poly      |
| 17 | | oveq2 5930 |
. . . . . . 7
           |
| 18 | 17 | sumeq1d 11531 |
. . . . . 6
                     
                     |
| 19 | 18 | mpteq2dv 4124 |
. . . . 5
                                               |
| 20 | 19 | eleq1d 2265 |
. . . 4
                        Poly 
                      Poly     |
| 21 | 20 | imbi2d 230 |
. . 3
  
                      Poly                          Poly      |
| 22 | | 0z 9337 |
. . . . . . . 8
 |
| 23 | | plyco.2 |
. . . . . . . . . . . . . 14
 Poly    |
| 24 | | plyf 14973 |
. . . . . . . . . . . . . 14
 Poly 
      |
| 25 | 23, 24 | syl 14 |
. . . . . . . . . . . . 13
       |
| 26 | 25 | ffvelcdmda 5697 |
. . . . . . . . . . . 12
 

      |
| 27 | 26 | exp0d 10759 |
. . . . . . . . . . 11
 

          |
| 28 | 27 | oveq2d 5938 |
. . . . . . . . . 10
 

                      |
| 29 | | plyco.1 |
. . . . . . . . . . . . . . 15
 Poly    |
| 30 | | plybss 14969 |
. . . . . . . . . . . . . . 15
 Poly 
  |
| 31 | 29, 30 | syl 14 |
. . . . . . . . . . . . . 14

  |
| 32 | | 0cnd 8019 |
. . . . . . . . . . . . . . 15
   |
| 33 | 32 | snssd 3767 |
. . . . . . . . . . . . . 14
     |
| 34 | 31, 33 | unssd 3339 |
. . . . . . . . . . . . 13
       |
| 35 | | plycolemc.a |
. . . . . . . . . . . . . 14
           |
| 36 | | 0nn0 9264 |
. . . . . . . . . . . . . . 15
 |
| 37 | 36 | a1i 9 |
. . . . . . . . . . . . . 14
   |
| 38 | 35, 37 | ffvelcdmd 5698 |
. . . . . . . . . . . . 13
           |
| 39 | 34, 38 | sseldd 3184 |
. . . . . . . . . . . 12
       |
| 40 | 39 | adantr 276 |
. . . . . . . . . . 11
 

      |
| 41 | 40 | mulridd 8043 |
. . . . . . . . . 10
 

            |
| 42 | 28, 41 | eqtrd 2229 |
. . . . . . . . 9
 

                    |
| 43 | 42, 40 | eqeltrd 2273 |
. . . . . . . 8
 

                |
| 44 | | fveq2 5558 |
. . . . . . . . . 10
           |
| 45 | | oveq2 5930 |
. . . . . . . . . 10
                   |
| 46 | 44, 45 | oveq12d 5940 |
. . . . . . . . 9
                               |
| 47 | 46 | fsum1 11577 |
. . . . . . . 8
                                                     |
| 48 | 22, 43, 47 | sylancr 414 |
. . . . . . 7
 

                                    |
| 49 | 48, 42 | eqtrd 2229 |
. . . . . 6
 

                          |
| 50 | 49 | mpteq2dva 4123 |
. . . . 5
                               |
| 51 | | fconstmpt 4710 |
. . . . 5
               |
| 52 | 50, 51 | eqtr4di 2247 |
. . . 4
                                 |
| 53 | | plyconst 14981 |
. . . . . 6
                       Poly        |
| 54 | 34, 38, 53 | syl2anc 411 |
. . . . 5
         Poly        |
| 55 | | plyun0 14972 |
. . . . 5
Poly 
    Poly   |
| 56 | 54, 55 | eleqtrdi 2289 |
. . . 4
         Poly    |
| 57 | 52, 56 | eqeltrd 2273 |
. . 3
                       Poly    |
| 58 | | simprr 531 |
. . . . . . . 8
 
                       Poly                          Poly    |
| 59 | 34 | adantr 276 |
. . . . . . . . . . . 12
 

      |
| 60 | | peano2nn0 9289 |
. . . . . . . . . . . . 13

    |
| 61 | | ffvelcdm 5695 |
. . . . . . . . . . . . 13
                         |
| 62 | 35, 60, 61 | syl2an 289 |
. . . . . . . . . . . 12
 

            |
| 63 | | plyconst 14981 |
. . . . . . . . . . . 12
                           Poly        |
| 64 | 59, 62, 63 | syl2anc 411 |
. . . . . . . . . . 11
 

          Poly 
      |
| 65 | 64, 55 | eleqtrdi 2289 |
. . . . . . . . . 10
 

          Poly    |
| 66 | | nn0p1nn 9288 |
. . . . . . . . . . . 12

    |
| 67 | | oveq2 5930 |
. . . . . . . . . . . . . . . 16
                   |
| 68 | 67 | mpteq2dv 4124 |
. . . . . . . . . . . . . . 15
                       |
| 69 | 68 | eleq1d 2265 |
. . . . . . . . . . . . . 14
            Poly 
          Poly     |
| 70 | 69 | imbi2d 230 |
. . . . . . . . . . . . 13
  
          Poly  
           Poly      |
| 71 | | oveq2 5930 |
. . . . . . . . . . . . . . . 16
                   |
| 72 | 71 | mpteq2dv 4124 |
. . . . . . . . . . . . . . 15
                       |
| 73 | 72 | eleq1d 2265 |
. . . . . . . . . . . . . 14
            Poly 
          Poly     |
| 74 | 73 | imbi2d 230 |
. . . . . . . . . . . . 13
  
          Poly  
           Poly      |
| 75 | | oveq2 5930 |
. . . . . . . . . . . . . . . 16
                       |
| 76 | 75 | mpteq2dv 4124 |
. . . . . . . . . . . . . . 15
                           |
| 77 | 76 | eleq1d 2265 |
. . . . . . . . . . . . . 14
              Poly 
            Poly     |
| 78 | 77 | imbi2d 230 |
. . . . . . . . . . . . 13
    
          Poly  
             Poly      |
| 79 | 26 | exp1d 10760 |
. . . . . . . . . . . . . . . 16
 

              |
| 80 | 79 | mpteq2dva 4123 |
. . . . . . . . . . . . . . 15
                   |
| 81 | 25 | feqmptd 5614 |
. . . . . . . . . . . . . . 15
         |
| 82 | 80, 81 | eqtr4d 2232 |
. . . . . . . . . . . . . 14
             |
| 83 | 82, 23 | eqeltrd 2273 |
. . . . . . . . . . . . 13
           Poly    |
| 84 | | simprr 531 |
. . . . . . . . . . . . . . . . . 18
 
           Poly              Poly    |
| 85 | 23 | adantr 276 |
. . . . . . . . . . . . . . . . . 18
 
           Poly   
Poly    |
| 86 | | plyco.3 |
. . . . . . . . . . . . . . . . . . 19
 

      |
| 87 | 86 | adantlr 477 |
. . . . . . . . . . . . . . . . . 18
              Poly           |
| 88 | | plyco.4 |
. . . . . . . . . . . . . . . . . . 19
 

      |
| 89 | 88 | adantlr 477 |
. . . . . . . . . . . . . . . . . 18
              Poly           |
| 90 | 84, 85, 87, 89 | plymul 14988 |
. . . . . . . . . . . . . . . . 17
 
           Poly                 Poly    |
| 91 | 90 | expr 375 |
. . . . . . . . . . . . . . . 16
 

           Poly               Poly     |
| 92 | | cnex 8003 |
. . . . . . . . . . . . . . . . . . . 20
 |
| 93 | 92 | a1i 9 |
. . . . . . . . . . . . . . . . . . 19
 

  |
| 94 | 26 | adantlr 477 |
. . . . . . . . . . . . . . . . . . . 20
           |
| 95 | | nnnn0 9256 |
. . . . . . . . . . . . . . . . . . . . 21
   |
| 96 | 95 | ad2antlr 489 |
. . . . . . . . . . . . . . . . . . . 20
       |
| 97 | 94, 96 | expcld 10765 |
. . . . . . . . . . . . . . . . . . 19
               |
| 98 | 25 | adantr 276 |
. . . . . . . . . . . . . . . . . . . 20
 

      |
| 99 | 98 | ffvelcdmda 5697 |
. . . . . . . . . . . . . . . . . . 19
           |
| 100 | | eqidd 2197 |
. . . . . . . . . . . . . . . . . . 19
 

                      |
| 101 | 81 | adantr 276 |
. . . . . . . . . . . . . . . . . . 19
 

        |
| 102 | 93, 97, 99, 100, 101 | offval2 6151 |
. . . . . . . . . . . . . . . . . 18
 

                               |
| 103 | 94, 96 | expp1d 10766 |
. . . . . . . . . . . . . . . . . . 19
                               |
| 104 | 103 | mpteq2dva 4123 |
. . . . . . . . . . . . . . . . . 18
 

                              |
| 105 | 102, 104 | eqtr4d 2232 |
. . . . . . . . . . . . . . . . 17
 

                           |
| 106 | 105 | eleq1d 2265 |
. . . . . . . . . . . . . . . 16
 

              Poly              Poly     |
| 107 | 91, 106 | sylibd 149 |
. . . . . . . . . . . . . . 15
 

           Poly              Poly     |
| 108 | 107 | expcom 116 |
. . . . . . . . . . . . . 14
             Poly 
            Poly      |
| 109 | 108 | a2d 26 |
. . . . . . . . . . . . 13
  
          Poly                Poly      |
| 110 | 70, 74, 78, 78, 83, 109 | nnind 9006 |
. . . . . . . . . . . 12
                Poly     |
| 111 | 66, 110 | syl 14 |
. . . . . . . . . . 11

             Poly     |
| 112 | 111 | impcom 125 |
. . . . . . . . . 10
 

            Poly    |
| 113 | 86 | adantlr 477 |
. . . . . . . . . 10
    
 
    |
| 114 | 88 | adantlr 477 |
. . . . . . . . . 10
    
 
    |
| 115 | 65, 112, 113, 114 | plymul 14988 |
. . . . . . . . 9
 

                         Poly    |
| 116 | 115 | adantrr 479 |
. . . . . . . 8
 
                       Poly                             Poly    |
| 117 | 86 | adantlr 477 |
. . . . . . . 8
                          Poly           |
| 118 | 58, 116, 117 | plyadd 14987 |
. . . . . . 7
 
                       Poly                                                      Poly    |
| 119 | 118 | expr 375 |
. . . . . 6
 

                       Poly                                                    Poly     |
| 120 | 92 | a1i 9 |
. . . . . . . . 9
 

  |
| 121 | | 0zd 9338 |
. . . . . . . . . . 11
       |
| 122 | | simplr 528 |
. . . . . . . . . . . 12
       |
| 123 | 122 | nn0zd 9446 |
. . . . . . . . . . 11
       |
| 124 | 121, 123 | fzfigd 10523 |
. . . . . . . . . 10
           |
| 125 | 29, 55 | eleqtrrdi 2290 |
. . . . . . . . . . . . . 14
 Poly 
      |
| 126 | | plybss 14969 |
. . . . . . . . . . . . . 14
 Poly 
          |
| 127 | 125, 126 | syl 14 |
. . . . . . . . . . . . 13
       |
| 128 | 127 | ad3antrrr 492 |
. . . . . . . . . . . 12
   


           |
| 129 | 35 | ad3antrrr 492 |
. . . . . . . . . . . . 13
   


               |
| 130 | | elfznn0 10189 |
. . . . . . . . . . . . . 14
       |
| 131 | 130 | adantl 277 |
. . . . . . . . . . . . 13
   


       |
| 132 | 129, 131 | ffvelcdmd 5698 |
. . . . . . . . . . . 12
   


               |
| 133 | 128, 132 | sseldd 3184 |
. . . . . . . . . . 11
   


           |
| 134 | 26 | ad4ant13 513 |
. . . . . . . . . . . 12
   


           |
| 135 | 134, 131 | expcld 10765 |
. . . . . . . . . . 11
   


               |
| 136 | 133, 135 | mulcld 8047 |
. . . . . . . . . 10
   


                     |
| 137 | 124, 136 | fsumcl 11565 |
. . . . . . . . 9
                           |
| 138 | 127 | ad2antrr 488 |
. . . . . . . . . . 11
     
     |
| 139 | 62 | adantr 276 |
. . . . . . . . . . 11
                 |
| 140 | 138, 139 | sseldd 3184 |
. . . . . . . . . 10
             |
| 141 | 26 | adantlr 477 |
. . . . . . . . . . 11
           |
| 142 | 60 | ad2antlr 489 |
. . . . . . . . . . 11
         |
| 143 | 141, 142 | expcld 10765 |
. . . . . . . . . 10
                 |
| 144 | 140, 143 | mulcld 8047 |
. . . . . . . . 9
                         |
| 145 | | eqidd 2197 |
. . . . . . . . 9
 

                                              |
| 146 | | fconstmpt 4710 |
. . . . . . . . . . 11
                   |
| 147 | 146 | a1i 9 |
. . . . . . . . . 10
 

                    |
| 148 | | eqidd 2197 |
. . . . . . . . . 10
 

                          |
| 149 | 120, 139,
143, 147, 148 | offval2 6151 |
. . . . . . . . 9
 

                                               |
| 150 | 120, 137,
144, 145, 149 | offval2 6151 |
. . . . . . . 8
 

                                                                                              |
| 151 | | nn0uz 9636 |
. . . . . . . . . . 11
     |
| 152 | 122, 151 | eleqtrdi 2289 |
. . . . . . . . . 10
           |
| 153 | 138 | adantr 276 |
. . . . . . . . . . . 12
   


             |
| 154 | 35 | ad3antrrr 492 |
. . . . . . . . . . . . 13
   


                 |
| 155 | | elfznn0 10189 |
. . . . . . . . . . . . . 14
         |
| 156 | 155 | adantl 277 |
. . . . . . . . . . . . 13
   


         |
| 157 | 154, 156 | ffvelcdmd 5698 |
. . . . . . . . . . . 12
   


                 |
| 158 | 153, 157 | sseldd 3184 |
. . . . . . . . . . 11
   


             |
| 159 | 141 | adantr 276 |
. . . . . . . . . . . 12
   


             |
| 160 | 159, 156 | expcld 10765 |
. . . . . . . . . . 11
   


                 |
| 161 | 158, 160 | mulcld 8047 |
. . . . . . . . . 10
   


                       |
| 162 | | fveq2 5558 |
. . . . . . . . . . 11
               |
| 163 | | oveq2 5930 |
. . . . . . . . . . 11
                       |
| 164 | 162, 163 | oveq12d 5940 |
. . . . . . . . . 10
                                     |
| 165 | 152, 161,
164 | fsump1 11585 |
. . . . . . . . 9
                                                                     |
| 166 | 165 | mpteq2dva 4123 |
. . . . . . . 8
 

                                                                    |
| 167 | 150, 166 | eqtr4d 2232 |
. . . . . . 7
 

                                                                            |
| 168 | 167 | eleq1d 2265 |
. . . . . 6
 

                                                   Poly                          Poly     |
| 169 | 119, 168 | sylibd 149 |
. . . . 5
 

                       Poly                          Poly     |
| 170 | 169 | expcom 116 |
. . . 4

                        Poly                          Poly      |
| 171 | 170 | a2d 26 |
. . 3

                        Poly   
                        Poly      |
| 172 | 6, 11, 16, 21, 57, 171 | nn0ind 9440 |
. 2

                       Poly     |
| 173 | 1, 172 | mpcom 36 |
1
                       Poly    |