Step | Hyp | Ref
| Expression |
1 | | plyco.2 |
. . . . 5
 Poly    |
2 | | plyf 23145 |
. . . . 5
 Poly 
      |
3 | 1, 2 | syl 17 |
. . . 4
       |
4 | 3 | ffvelrnda 6020 |
. . 3
 

      |
5 | 3 | feqmptd 5916 |
. . 3
         |
6 | | plyco.1 |
. . . 4
 Poly    |
7 | | eqid 2450 |
. . . . 5
coeff  coeff   |
8 | | eqid 2450 |
. . . . 5
deg  deg   |
9 | 7, 8 | coeid 23185 |
. . . 4
 Poly 

    deg      coeff             |
10 | 6, 9 | syl 17 |
. . 3
      deg      coeff             |
11 | | oveq1 6295 |
. . . . 5
                   |
12 | 11 | oveq2d 6304 |
. . . 4
       coeff            coeff                |
13 | 12 | sumeq2sdv 13763 |
. . 3
         deg      coeff          
   deg      coeff                |
14 | 4, 5, 10, 13 | fmptco 6054 |
. 2
        deg      coeff                 |
15 | | dgrcl 23180 |
. . . 4
 Poly 
deg    |
16 | 6, 15 | syl 17 |
. . 3
 deg    |
17 | | oveq2 6296 |
. . . . . . . 8
           |
18 | 17 | sumeq1d 13760 |
. . . . . . 7
         coeff                      coeff                |
19 | 18 | mpteq2dv 4489 |
. . . . . 6
          coeff                        coeff                 |
20 | 19 | eleq1d 2512 |
. . . . 5
           coeff               Poly           coeff               Poly     |
21 | 20 | imbi2d 318 |
. . . 4
  
         coeff               Poly  
          coeff               Poly      |
22 | | oveq2 6296 |
. . . . . . . 8
           |
23 | 22 | sumeq1d 13760 |
. . . . . . 7
         coeff                      coeff                |
24 | 23 | mpteq2dv 4489 |
. . . . . 6
          coeff                        coeff                 |
25 | 24 | eleq1d 2512 |
. . . . 5
           coeff               Poly           coeff               Poly     |
26 | 25 | imbi2d 318 |
. . . 4
  
         coeff               Poly  
          coeff               Poly      |
27 | | oveq2 6296 |
. . . . . . . 8
               |
28 | 27 | sumeq1d 13760 |
. . . . . . 7
           coeff                        coeff                |
29 | 28 | mpteq2dv 4489 |
. . . . . 6
            coeff                          coeff                 |
30 | 29 | eleq1d 2512 |
. . . . 5
             coeff               Poly             coeff               Poly     |
31 | 30 | imbi2d 318 |
. . . 4
    
         coeff               Poly  
            coeff               Poly      |
32 | | oveq2 6296 |
. . . . . . . 8
 deg 
       deg     |
33 | 32 | sumeq1d 13760 |
. . . . . . 7
 deg 
        coeff                  deg      coeff                |
34 | 33 | mpteq2dv 4489 |
. . . . . 6
 deg 
         coeff                    deg      coeff                 |
35 | 34 | eleq1d 2512 |
. . . . 5
 deg 
          coeff               Poly       deg      coeff               Poly     |
36 | 35 | imbi2d 318 |
. . . 4
 deg 
           coeff               Poly  
      deg      coeff               Poly      |
37 | | 0z 10945 |
. . . . . . . . 9
 |
38 | 4 | exp0d 12407 |
. . . . . . . . . . . 12
 

          |
39 | 38 | oveq2d 6304 |
. . . . . . . . . . 11
 

  coeff                coeff        |
40 | | plybss 23141 |
. . . . . . . . . . . . . . . 16
 Poly 
  |
41 | 6, 40 | syl 17 |
. . . . . . . . . . . . . . 15

  |
42 | | 0cnd 9633 |
. . . . . . . . . . . . . . . 16
   |
43 | 42 | snssd 4116 |
. . . . . . . . . . . . . . 15
     |
44 | 41, 43 | unssd 3609 |
. . . . . . . . . . . . . 14
       |
45 | 7 | coef 23177 |
. . . . . . . . . . . . . . . 16
 Poly 
coeff            |
46 | 6, 45 | syl 17 |
. . . . . . . . . . . . . . 15
 coeff            |
47 | | 0nn0 10881 |
. . . . . . . . . . . . . . 15
 |
48 | | ffvelrn 6018 |
. . . . . . . . . . . . . . 15
  coeff         
  coeff           |
49 | 46, 47, 48 | sylancl 667 |
. . . . . . . . . . . . . 14
  coeff           |
50 | 44, 49 | sseldd 3432 |
. . . . . . . . . . . . 13
  coeff       |
51 | 50 | adantr 467 |
. . . . . . . . . . . 12
 

 coeff       |
52 | 51 | mulid1d 9657 |
. . . . . . . . . . 11
 

  coeff       coeff       |
53 | 39, 52 | eqtrd 2484 |
. . . . . . . . . 10
 

  coeff               coeff       |
54 | 53, 51 | eqeltrd 2528 |
. . . . . . . . 9
 

  coeff                |
55 | | fveq2 5863 |
. . . . . . . . . . 11
  coeff      coeff       |
56 | | oveq2 6296 |
. . . . . . . . . . 11
                   |
57 | 55, 56 | oveq12d 6306 |
. . . . . . . . . 10
   coeff                coeff                |
58 | 57 | fsum1 13801 |
. . . . . . . . 9
    coeff                       coeff                coeff                |
59 | 37, 54, 58 | sylancr 668 |
. . . . . . . 8
 

        coeff                coeff                |
60 | 59, 53 | eqtrd 2484 |
. . . . . . 7
 

        coeff               coeff       |
61 | 60 | mpteq2dva 4488 |
. . . . . 6
          coeff                 coeff        |
62 | | fconstmpt 4877 |
. . . . . 6
   coeff         coeff       |
63 | 61, 62 | syl6eqr 2502 |
. . . . 5
          coeff                  coeff         |
64 | | plyconst 23153 |
. . . . . . 7
       coeff             coeff       Poly        |
65 | 44, 49, 64 | syl2anc 666 |
. . . . . 6
    coeff       Poly        |
66 | | plyun0 23144 |
. . . . . 6
Poly 
    Poly   |
67 | 65, 66 | syl6eleq 2538 |
. . . . 5
    coeff       Poly    |
68 | 63, 67 | eqeltrd 2528 |
. . . 4
          coeff               Poly    |
69 | | simprr 765 |
. . . . . . . . 9
 
          coeff               Poly             coeff               Poly    |
70 | 44 | adantr 467 |
. . . . . . . . . . . . 13
 

      |
71 | | peano2nn0 10907 |
. . . . . . . . . . . . . 14

    |
72 | | ffvelrn 6018 |
. . . . . . . . . . . . . 14
  coeff              coeff             |
73 | 46, 71, 72 | syl2an 480 |
. . . . . . . . . . . . 13
 

 coeff             |
74 | | plyconst 23153 |
. . . . . . . . . . . . 13
       coeff               coeff         Poly        |
75 | 70, 73, 74 | syl2anc 666 |
. . . . . . . . . . . 12
 

   coeff         Poly        |
76 | 75, 66 | syl6eleq 2538 |
. . . . . . . . . . 11
 

   coeff         Poly    |
77 | | nn0p1nn 10906 |
. . . . . . . . . . . . 13

    |
78 | | oveq2 6296 |
. . . . . . . . . . . . . . . . 17
                   |
79 | 78 | mpteq2dv 4489 |
. . . . . . . . . . . . . . . 16
                       |
80 | 79 | eleq1d 2512 |
. . . . . . . . . . . . . . 15
            Poly 
          Poly     |
81 | 80 | imbi2d 318 |
. . . . . . . . . . . . . 14
  
          Poly  
           Poly      |
82 | | oveq2 6296 |
. . . . . . . . . . . . . . . . 17
                   |
83 | 82 | mpteq2dv 4489 |
. . . . . . . . . . . . . . . 16
                       |
84 | 83 | eleq1d 2512 |
. . . . . . . . . . . . . . 15
            Poly 
          Poly     |
85 | 84 | imbi2d 318 |
. . . . . . . . . . . . . 14
  
          Poly  
           Poly      |
86 | | oveq2 6296 |
. . . . . . . . . . . . . . . . 17
                       |
87 | 86 | mpteq2dv 4489 |
. . . . . . . . . . . . . . . 16
                           |
88 | 87 | eleq1d 2512 |
. . . . . . . . . . . . . . 15
              Poly 
            Poly     |
89 | 88 | imbi2d 318 |
. . . . . . . . . . . . . 14
    
          Poly  
             Poly      |
90 | 4 | exp1d 12408 |
. . . . . . . . . . . . . . . . 17
 

              |
91 | 90 | mpteq2dva 4488 |
. . . . . . . . . . . . . . . 16
                   |
92 | 91, 5 | eqtr4d 2487 |
. . . . . . . . . . . . . . 15
             |
93 | 92, 1 | eqeltrd 2528 |
. . . . . . . . . . . . . 14
           Poly    |
94 | | simprr 765 |
. . . . . . . . . . . . . . . . . . 19
 
           Poly              Poly    |
95 | 1 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
 
           Poly   
Poly    |
96 | | plyco.3 |
. . . . . . . . . . . . . . . . . . . 20
 

      |
97 | 96 | adantlr 720 |
. . . . . . . . . . . . . . . . . . 19
              Poly           |
98 | | plyco.4 |
. . . . . . . . . . . . . . . . . . . 20
 

      |
99 | 98 | adantlr 720 |
. . . . . . . . . . . . . . . . . . 19
              Poly           |
100 | 94, 95, 97, 99 | plymul 23165 |
. . . . . . . . . . . . . . . . . 18
 
           Poly                 Poly    |
101 | 100 | expr 619 |
. . . . . . . . . . . . . . . . 17
 

           Poly               Poly     |
102 | | cnex 9617 |
. . . . . . . . . . . . . . . . . . . . 21
 |
103 | 102 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
 

  |
104 | | ovex 6316 |
. . . . . . . . . . . . . . . . . . . . 21
         |
105 | 104 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
               |
106 | 4 | adantlr 720 |
. . . . . . . . . . . . . . . . . . . 20
           |
107 | | eqidd 2451 |
. . . . . . . . . . . . . . . . . . . 20
 

                      |
108 | 5 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
 

        |
109 | 103, 105,
106, 107, 108 | offval2 6545 |
. . . . . . . . . . . . . . . . . . 19
 

                               |
110 | | nnnn0 10873 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
111 | 110 | ad2antlr 732 |
. . . . . . . . . . . . . . . . . . . . 21
       |
112 | 106, 111 | expp1d 12414 |
. . . . . . . . . . . . . . . . . . . 20
                               |
113 | 112 | mpteq2dva 4488 |
. . . . . . . . . . . . . . . . . . 19
 

                              |
114 | 109, 113 | eqtr4d 2487 |
. . . . . . . . . . . . . . . . . 18
 

                           |
115 | 114 | eleq1d 2512 |
. . . . . . . . . . . . . . . . 17
 

              Poly              Poly     |
116 | 101, 115 | sylibd 218 |
. . . . . . . . . . . . . . . 16
 

           Poly              Poly     |
117 | 116 | expcom 437 |
. . . . . . . . . . . . . . 15
             Poly 
            Poly      |
118 | 117 | a2d 29 |
. . . . . . . . . . . . . 14
  
          Poly                Poly      |
119 | 81, 85, 89, 89, 93, 118 | nnind 10624 |
. . . . . . . . . . . . 13
                Poly     |
120 | 77, 119 | syl 17 |
. . . . . . . . . . . 12

             Poly     |
121 | 120 | impcom 432 |
. . . . . . . . . . 11
 

            Poly    |
122 | 96 | adantlr 720 |
. . . . . . . . . . 11
    
 
    |
123 | 98 | adantlr 720 |
. . . . . . . . . . 11
    
 
    |
124 | 76, 121, 122, 123 | plymul 23165 |
. . . . . . . . . 10
 

    coeff                       Poly    |
125 | 124 | adantrr 722 |
. . . . . . . . 9
 
          coeff               Poly        coeff                       Poly    |
126 | 96 | adantlr 720 |
. . . . . . . . 9
             coeff               Poly    
 
    |
127 | 69, 125, 126 | plyadd 23164 |
. . . . . . . 8
 
          coeff               Poly              coeff                    coeff                        Poly    |
128 | 127 | expr 619 |
. . . . . . 7
 

          coeff               Poly            coeff                    coeff                        Poly     |
129 | 102 | a1i 11 |
. . . . . . . . . 10
 

  |
130 | | sumex 13747 |
. . . . . . . . . . 11
        coeff               |
131 | 130 | a1i 11 |
. . . . . . . . . 10
             coeff                |
132 | | ovex 6316 |
. . . . . . . . . . 11
  coeff                   |
133 | 132 | a1i 11 |
. . . . . . . . . 10
       coeff                    |
134 | | eqidd 2451 |
. . . . . . . . . 10
 

         coeff                        coeff                 |
135 | | fvex 5873 |
. . . . . . . . . . . 12
 coeff        |
136 | 135 | a1i 11 |
. . . . . . . . . . 11
      coeff         |
137 | | ovex 6316 |
. . . . . . . . . . . 12
           |
138 | 137 | a1i 11 |
. . . . . . . . . . 11
                 |
139 | | fconstmpt 4877 |
. . . . . . . . . . . 12
   coeff           coeff         |
140 | 139 | a1i 11 |
. . . . . . . . . . 11
 

   coeff           coeff          |
141 | | eqidd 2451 |
. . . . . . . . . . 11
 

                          |
142 | 129, 136,
138, 140, 141 | offval2 6545 |
. . . . . . . . . 10
 

    coeff                          coeff                     |
143 | 129, 131,
133, 134, 142 | offval2 6545 |
. . . . . . . . 9
 

          coeff                    coeff                                  coeff                coeff                      |
144 | | simplr 761 |
. . . . . . . . . . . 12
       |
145 | | nn0uz 11190 |
. . . . . . . . . . . 12
     |
146 | 144, 145 | syl6eleq 2538 |
. . . . . . . . . . 11
           |
147 | 7 | coef3 23179 |
. . . . . . . . . . . . . . 15
 Poly 
coeff        |
148 | 6, 147 | syl 17 |
. . . . . . . . . . . . . 14
 coeff        |
149 | 148 | ad2antrr 731 |
. . . . . . . . . . . . 13
     coeff        |
150 | | elfznn0 11884 |
. . . . . . . . . . . . 13
         |
151 | | ffvelrn 6018 |
. . . . . . . . . . . . 13
  coeff        coeff       |
152 | 149, 150,
151 | syl2an 480 |
. . . . . . . . . . . 12
   


        coeff       |
153 | 4 | adantlr 720 |
. . . . . . . . . . . . 13
           |
154 | | expcl 12287 |
. . . . . . . . . . . . 13
     
           |
155 | 153, 150,
154 | syl2an 480 |
. . . . . . . . . . . 12
   


                 |
156 | 152, 155 | mulcld 9660 |
. . . . . . . . . . 11
   


         coeff                |
157 | | fveq2 5863 |
. . . . . . . . . . . 12
    coeff      coeff         |
158 | | oveq2 6296 |
. . . . . . . . . . . 12
                       |
159 | 157, 158 | oveq12d 6306 |
. . . . . . . . . . 11
     coeff                coeff                    |
160 | 146, 156,
159 | fsump1 13810 |
. . . . . . . . . 10
               coeff                       coeff                coeff                     |
161 | 160 | mpteq2dva 4488 |
. . . . . . . . 9
 

           coeff                 
       coeff                coeff                      |
162 | 143, 161 | eqtr4d 2487 |
. . . . . . . 8
 

          coeff                    coeff                                   coeff                 |
163 | 162 | eleq1d 2512 |
. . . . . . 7
 

           coeff                    coeff                        Poly             coeff               Poly     |
164 | 128, 163 | sylibd 218 |
. . . . . 6
 

          coeff               Poly             coeff               Poly     |
165 | 164 | expcom 437 |
. . . . 5

           coeff               Poly             coeff               Poly      |
166 | 165 | a2d 29 |
. . . 4

           coeff               Poly   
           coeff               Poly      |
167 | 21, 26, 31, 36, 68, 166 | nn0ind 11027 |
. . 3
 deg        deg      coeff               Poly     |
168 | 16, 167 | mpcom 37 |
. 2
      deg      coeff               Poly    |
169 | 14, 168 | eqeltrd 2528 |
1
   Poly    |