Step | Hyp | Ref
| Expression |
1 | | eldifi 3555 |
. . . . 5
  Poly 
   
Poly    |
2 | | ax-resscn 9596 |
. . . . . . 7
 |
3 | | 1re 9642 |
. . . . . . 7
 |
4 | | plyid 23163 |
. . . . . . 7
 
 
Poly    |
5 | 2, 3, 4 | mp2an 678 |
. . . . . 6
 Poly   |
6 | 5 | a1i 11 |
. . . . 5
  Poly 
    
Poly    |
7 | | simprl 764 |
. . . . . 6
   Poly        
  |
8 | | simprr 766 |
. . . . . 6
   Poly           |
9 | 7, 8 | readdcld 9670 |
. . . . 5
   Poly             |
10 | 7, 8 | remulcld 9671 |
. . . . 5
   Poly             |
11 | 1, 6, 9, 10 | plymul 23172 |
. . . 4
  Poly 
        Poly    |
12 | | 0re 9643 |
. . . 4
 |
13 | | eqid 2451 |
. . . . 5
coeff 
    coeff       |
14 | 13 | coef2 23185 |
. . . 4
      Poly   coeff            |
15 | 11, 12, 14 | sylancl 668 |
. . 3
  Poly 
    coeff  
         |
16 | 15 | feqmptd 5918 |
. 2
  Poly 
    coeff  
     coeff  
         |
17 | | cnex 9620 |
. . . . . . . . 9
 |
18 | 17 | a1i 11 |
. . . . . . . 8
  Poly 
      |
19 | | plyf 23152 |
. . . . . . . . 9
 Poly        |
20 | 1, 19 | syl 17 |
. . . . . . . 8
  Poly 
          |
21 | | plyf 23152 |
. . . . . . . . . 10
  Poly 
       |
22 | 5, 21 | ax-mp 5 |
. . . . . . . . 9
      |
23 | 22 | a1i 11 |
. . . . . . . 8
  Poly 
           |
24 | | simprl 764 |
. . . . . . . . 9
   Poly        
  |
25 | | simprr 766 |
. . . . . . . . 9
   Poly           |
26 | 24, 25 | mulcomd 9664 |
. . . . . . . 8
   Poly               |
27 | 18, 20, 23, 26 | caofcom 6563 |
. . . . . . 7
  Poly 
              |
28 | 27 | fveq2d 5869 |
. . . . . 6
  Poly 
    coeff  
   coeff        |
29 | 28 | fveq1d 5867 |
. . . . 5
  Poly 
     coeff          coeff           |
30 | 29 | adantr 467 |
. . . 4
   Poly        coeff 
        coeff           |
31 | 5 | a1i 11 |
. . . . . 6
   Poly        Poly    |
32 | 1 | adantr 467 |
. . . . . 6
   Poly       Poly    |
33 | | simpr 463 |
. . . . . 6
   Poly         |
34 | | eqid 2451 |
. . . . . . 7
coeff   coeff    |
35 | | eqid 2451 |
. . . . . . 7
coeff  coeff   |
36 | 34, 35 | coemul 23206 |
. . . . . 6
   Poly  Poly 
  coeff                 coeff       coeff          |
37 | 31, 32, 33, 36 | syl3anc 1268 |
. . . . 5
   Poly        coeff                 coeff       coeff          |
38 | | elfznn0 11887 |
. . . . . . . . . 10
       |
39 | | coeidp 23217 |
. . . . . . . . . 10

 coeff             |
40 | 38, 39 | syl 17 |
. . . . . . . . 9
      coeff             |
41 | 40 | oveq1d 6305 |
. . . . . . . 8
       coeff       coeff               coeff          |
42 | | ovif 6373 |
. . . . . . . 8
       coeff             coeff           coeff          |
43 | 41, 42 | syl6eq 2501 |
. . . . . . 7
       coeff       coeff             coeff           coeff           |
44 | 43 | adantl 468 |
. . . . . 6
    Poly     
        coeff       coeff             coeff           coeff           |
45 | 44 | sumeq2dv 13769 |
. . . . 5
   Poly               coeff       coeff                   coeff           coeff           |
46 | | elsn 3982 |
. . . . . . . . . 10
     |
47 | 46 | bicomi 206 |
. . . . . . . . 9

    |
48 | 47 | a1i 11 |
. . . . . . . 8
    Poly     
            |
49 | 35 | coef2 23185 |
. . . . . . . . . . . . 13
  Poly 
 coeff        |
50 | 1, 12, 49 | sylancl 668 |
. . . . . . . . . . . 12
  Poly 
    coeff        |
51 | 50 | ad2antrr 732 |
. . . . . . . . . . 11
    Poly     
      coeff        |
52 | | fznn0sub 11831 |
. . . . . . . . . . . 12
         |
53 | 52 | adantl 468 |
. . . . . . . . . . 11
    Poly     
          |
54 | 51, 53 | ffvelrnd 6023 |
. . . . . . . . . 10
    Poly     
       coeff         |
55 | 54 | recnd 9669 |
. . . . . . . . 9
    Poly     
       coeff         |
56 | 55 | mulid2d 9661 |
. . . . . . . 8
    Poly     
        coeff         coeff         |
57 | 55 | mul02d 9831 |
. . . . . . . 8
    Poly     
        coeff          |
58 | 48, 56, 57 | ifbieq12d 3908 |
. . . . . . 7
    Poly     
           coeff           coeff               coeff           |
59 | 58 | sumeq2dv 13769 |
. . . . . 6
   Poly                  coeff           coeff                     coeff           |
60 | | eqeq2 2462 |
. . . . . . 7
      coeff                     coeff         
           coeff              coeff           |
61 | | eqeq2 2462 |
. . . . . . 7
  coeff            coeff                     coeff          coeff                   coeff              coeff           |
62 | | oveq2 6298 |
. . . . . . . . . . 11
           |
63 | | 0z 10948 |
. . . . . . . . . . . 12
 |
64 | | fzsn 11840 |
. . . . . . . . . . . 12
         |
65 | 63, 64 | ax-mp 5 |
. . . . . . . . . . 11
       |
66 | 62, 65 | syl6eq 2501 |
. . . . . . . . . 10
         |
67 | | elsni 3993 |
. . . . . . . . . . . . 13
     |
68 | 67 | adantl 468 |
. . . . . . . . . . . 12
       |
69 | | ax-1ne0 9608 |
. . . . . . . . . . . . . 14
 |
70 | 69 | nesymi 2681 |
. . . . . . . . . . . . 13
 |
71 | | eqeq1 2455 |
. . . . . . . . . . . . 13
     |
72 | 70, 71 | mtbiri 305 |
. . . . . . . . . . . 12

  |
73 | 68, 72 | syl 17 |
. . . . . . . . . . 11
    
  |
74 | 47 | notbii 298 |
. . . . . . . . . . . 12

    |
75 | 74 | biimpi 198 |
. . . . . . . . . . 11

    |
76 | | iffalse 3890 |
. . . . . . . . . . 11
  
      coeff           |
77 | 73, 75, 76 | 3syl 18 |
. . . . . . . . . 10
           coeff           |
78 | 66, 77 | sumeq12rdv 13773 |
. . . . . . . . 9
             coeff               |
79 | | snfi 7650 |
. . . . . . . . . . 11
   |
80 | 79 | olci 393 |
. . . . . . . . . 10
           |
81 | | sumz 13788 |
. . . . . . . . . 10
          
      |
82 | 80, 81 | ax-mp 5 |
. . . . . . . . 9
     |
83 | 78, 82 | syl6eq 2501 |
. . . . . . . 8
             coeff           |
84 | 83 | adantl 468 |
. . . . . . 7
    Poly     
              coeff           |
85 | | simpll 760 |
. . . . . . . 8
    Poly     
 
 Poly        |
86 | 33 | adantr 467 |
. . . . . . . . 9
    Poly     
 
  |
87 | | simpr 463 |
. . . . . . . . . 10
    Poly     
 
  |
88 | 87 | neqned 2631 |
. . . . . . . . 9
    Poly     
    |
89 | | elnnne0 10883 |
. . . . . . . . 9

    |
90 | 86, 88, 89 | sylanbrc 670 |
. . . . . . . 8
    Poly     
 
  |
91 | | 1nn0 10885 |
. . . . . . . . . . . . 13
 |
92 | 91 | a1i 11 |
. . . . . . . . . . . 12
   Poly         |
93 | | simpr 463 |
. . . . . . . . . . . . 13
   Poly         |
94 | 93 | nnnn0d 10925 |
. . . . . . . . . . . 12
   Poly         |
95 | 93 | nnge1d 10652 |
. . . . . . . . . . . 12
   Poly         |
96 | | elfz2nn0 11885 |
. . . . . . . . . . . 12
    

   |
97 | 92, 94, 95, 96 | syl3anbrc 1192 |
. . . . . . . . . . 11
   Poly             |
98 | 97 | snssd 4117 |
. . . . . . . . . 10
   Poly               |
99 | 50 | ad2antrr 732 |
. . . . . . . . . . . . 13
    Poly     

   coeff        |
100 | | oveq2 6298 |
. . . . . . . . . . . . . . . 16
       |
101 | 46, 100 | sylbi 199 |
. . . . . . . . . . . . . . 15
         |
102 | 101 | adantl 468 |
. . . . . . . . . . . . . 14
    Poly     

         |
103 | | nnm1nn0 10911 |
. . . . . . . . . . . . . . 15
     |
104 | 103 | ad2antlr 733 |
. . . . . . . . . . . . . 14
    Poly     

       |
105 | 102, 104 | eqeltrd 2529 |
. . . . . . . . . . . . 13
    Poly     

       |
106 | 99, 105 | ffvelrnd 6023 |
. . . . . . . . . . . 12
    Poly     

    coeff         |
107 | 106 | recnd 9669 |
. . . . . . . . . . 11
    Poly     

    coeff         |
108 | 107 | ralrimiva 2802 |
. . . . . . . . . 10
   Poly           coeff         |
109 | | fzfi 12185 |
. . . . . . . . . . . 12
     |
110 | 109 | olci 393 |
. . . . . . . . . . 11
               |
111 | 110 | a1i 11 |
. . . . . . . . . 10
   Poly                       |
112 | | sumss2 13792 |
. . . . . . . . . 10
         
   coeff                      
    coeff       
           coeff           |
113 | 98, 108, 111, 112 | syl21anc 1267 |
. . . . . . . . 9
   Poly           coeff                   coeff           |
114 | 50 | adantr 467 |
. . . . . . . . . . . 12
   Poly       coeff        |
115 | 103 | adantl 468 |
. . . . . . . . . . . 12
   Poly           |
116 | 114, 115 | ffvelrnd 6023 |
. . . . . . . . . . 11
   Poly        coeff         |
117 | 116 | recnd 9669 |
. . . . . . . . . 10
   Poly        coeff         |
118 | 100 | fveq2d 5869 |
. . . . . . . . . . 11
  coeff        coeff         |
119 | 118 | sumsn 13807 |
. . . . . . . . . 10
   coeff            coeff        coeff         |
120 | 3, 117, 119 | sylancr 669 |
. . . . . . . . 9
   Poly           coeff        coeff         |
121 | 113, 120 | eqtr3d 2487 |
. . . . . . . 8
   Poly                   coeff          coeff         |
122 | 85, 90, 121 | syl2anc 667 |
. . . . . . 7
    Poly     
              coeff          coeff         |
123 | 60, 61, 84, 122 | ifbothda 3916 |
. . . . . 6
   Poly                   coeff              coeff          |
124 | 59, 123 | eqtrd 2485 |
. . . . 5
   Poly                  coeff           coeff              coeff          |
125 | 37, 45, 124 | 3eqtrd 2489 |
. . . 4
   Poly        coeff              coeff          |
126 | 30, 125 | eqtrd 2485 |
. . 3
   Poly        coeff 
            coeff          |
127 | 126 | mpteq2dva 4489 |
. 2
  Poly 
      coeff  
             coeff           |
128 | 16, 127 | eqtrd 2485 |
1
  Poly 
    coeff  
         coeff           |