Step | Hyp | Ref
| Expression |
1 | | bpolydiflem.1 |
. . . . 5
   |
2 | 1 | nnnn0d 10949 |
. . . 4
   |
3 | | bpolydiflem.2 |
. . . . 5
   |
4 | | peano2cn 9823 |
. . . . 5
 
   |
5 | 3, 4 | syl 17 |
. . . 4
     |
6 | | bpolyval 14179 |
. . . 4
  
   BernPoly 
                      BernPoly
            |
7 | 2, 5, 6 | syl2anc 673 |
. . 3
  BernPoly
                       BernPoly             |
8 | | bpolyval 14179 |
. . . 4
 
  BernPoly
                   BernPoly           |
9 | 2, 3, 8 | syl2anc 673 |
. . 3
  BernPoly
                   BernPoly           |
10 | 7, 9 | oveq12d 6326 |
. 2
   BernPoly 
   BernPoly                        BernPoly                             BernPoly            |
11 | 5, 2 | expcld 12454 |
. . 3
         |
12 | | fzfid 12224 |
. . . 4
    
    |
13 | | elfzelz 11826 |
. . . . . . 7
         |
14 | | bccl 12545 |
. . . . . . 7
 
     |
15 | 2, 13, 14 | syl2an 485 |
. . . . . 6
 
   
       |
16 | 15 | nn0cnd 10951 |
. . . . 5
 
   
       |
17 | | elfznn0 11913 |
. . . . . . 7
         |
18 | | bpolycl 14182 |
. . . . . . 7
  
   BernPoly 
    |
19 | 17, 5, 18 | syl2anr 486 |
. . . . . 6
 
   
    BernPoly      |
20 | | fzssp1 11867 |
. . . . . . . . . . 11
               |
21 | 1 | nncnd 10647 |
. . . . . . . . . . . . 13
   |
22 | | ax-1cn 9615 |
. . . . . . . . . . . . 13
 |
23 | | npcan 9904 |
. . . . . . . . . . . . 13
 
       |
24 | 21, 22, 23 | sylancl 675 |
. . . . . . . . . . . 12
       |
25 | 24 | oveq2d 6324 |
. . . . . . . . . . 11
               |
26 | 20, 25 | syl5sseq 3466 |
. . . . . . . . . 10
    
 
      |
27 | 26 | sselda 3418 |
. . . . . . . . 9
 
   
         |
28 | | fznn0sub 11857 |
. . . . . . . . 9
     
   |
29 | 27, 28 | syl 17 |
. . . . . . . 8
 
   
   
   |
30 | | nn0p1nn 10933 |
. . . . . . . 8
  
      |
31 | 29, 30 | syl 17 |
. . . . . . 7
 
   
         |
32 | 31 | nncnd 10647 |
. . . . . 6
 
   
         |
33 | 31 | nnne0d 10676 |
. . . . . 6
 
   
         |
34 | 19, 32, 33 | divcld 10405 |
. . . . 5
 
   
     BernPoly
          |
35 | 16, 34 | mulcld 9681 |
. . . 4
 
   
        BernPoly            |
36 | 12, 35 | fsumcl 13876 |
. . 3
              BernPoly
           |
37 | 3, 2 | expcld 12454 |
. . 3
       |
38 | | bpolycl 14182 |
. . . . . . 7
 
  BernPoly    |
39 | 17, 3, 38 | syl2anr 486 |
. . . . . 6
 
   
    BernPoly    |
40 | 39, 32, 33 | divcld 10405 |
. . . . 5
 
   
     BernPoly
        |
41 | 16, 40 | mulcld 9681 |
. . . 4
 
   
        BernPoly          |
42 | 12, 41 | fsumcl 13876 |
. . 3
              BernPoly
         |
43 | 11, 36, 37, 42 | sub4d 10054 |
. 2
                      BernPoly                             BernPoly                                     BernPoly
                      BernPoly
           |
44 | | addcom 9837 |
. . . . . . . . . . 11
 
       |
45 | 3, 22, 44 | sylancl 675 |
. . . . . . . . . 10
       |
46 | 45 | oveq1d 6323 |
. . . . . . . . 9
               |
47 | | binom1p 13966 |
. . . . . . . . . 10
 
                       |
48 | 3, 2, 47 | syl2anc 673 |
. . . . . . . . 9
                       |
49 | 46, 48 | eqtrd 2505 |
. . . . . . . 8
                       |
50 | | nn0uz 11217 |
. . . . . . . . . 10
     |
51 | 2, 50 | syl6eleq 2559 |
. . . . . . . . 9
       |
52 | | bccl2 12546 |
. . . . . . . . . . . 12
         |
53 | 52 | adantl 473 |
. . . . . . . . . . 11
 
         |
54 | 53 | nncnd 10647 |
. . . . . . . . . 10
 
         |
55 | | elfznn0 11913 |
. . . . . . . . . . 11
       |
56 | | expcl 12328 |
. . . . . . . . . . 11
 
       |
57 | 3, 55, 56 | syl2an 485 |
. . . . . . . . . 10
 
           |
58 | 54, 57 | mulcld 9681 |
. . . . . . . . 9
 
               |
59 | | oveq2 6316 |
. . . . . . . . . 10
       |
60 | | oveq2 6316 |
. . . . . . . . . 10
           |
61 | 59, 60 | oveq12d 6326 |
. . . . . . . . 9
                   |
62 | 51, 58, 61 | fsumm1 13889 |
. . . . . . . 8
 
                  
                      |
63 | | bcnn 12535 |
. . . . . . . . . . . 12

    |
64 | 2, 63 | syl 17 |
. . . . . . . . . . 11
     |
65 | 64 | oveq1d 6323 |
. . . . . . . . . 10
                 |
66 | 37 | mulid2d 9679 |
. . . . . . . . . 10
             |
67 | 65, 66 | eqtrd 2505 |
. . . . . . . . 9
               |
68 | 67 | oveq2d 6324 |
. . . . . . . 8
                                                   |
69 | 49, 62, 68 | 3eqtrd 2509 |
. . . . . . 7
                               |
70 | 69 | oveq1d 6323 |
. . . . . 6
                                           |
71 | 26 | sselda 3418 |
. . . . . . . . 9
 
   
         |
72 | 71, 58 | syldan 478 |
. . . . . . . 8
 
   
             |
73 | 12, 72 | fsumcl 13876 |
. . . . . . 7
 
                 |
74 | 73, 37 | pncand 10006 |
. . . . . 6
       
                                       |
75 | 70, 74 | eqtrd 2505 |
. . . . 5
                               |
76 | | nnm1nn0 10935 |
. . . . . . . 8
 
   |
77 | 1, 76 | syl 17 |
. . . . . . 7
     |
78 | 77, 50 | syl6eleq 2559 |
. . . . . 6
         |
79 | | oveq2 6316 |
. . . . . . 7
      
    |
80 | | oveq2 6316 |
. . . . . . 7
          
    |
81 | 79, 80 | oveq12d 6326 |
. . . . . 6
                   
     |
82 | 78, 72, 81 | fsumm1 13889 |
. . . . 5
 
                                    
            |
83 | | 1cnd 9677 |
. . . . . . . . . 10
   |
84 | 21, 83, 83 | subsub4d 10036 |
. . . . . . . . 9
           |
85 | | df-2 10690 |
. . . . . . . . . 10
   |
86 | 85 | oveq2i 6319 |
. . . . . . . . 9
       |
87 | 84, 86 | syl6eqr 2523 |
. . . . . . . 8
         |
88 | 87 | oveq2d 6324 |
. . . . . . 7
                 |
89 | 88 | sumeq1d 13844 |
. . . . . 6
 
                                   |
90 | | bcnm1 12550 |
. . . . . . . 8

      |
91 | 2, 90 | syl 17 |
. . . . . . 7
  
    |
92 | 91 | oveq1d 6323 |
. . . . . 6
   
                   |
93 | 89, 92 | oveq12d 6326 |
. . . . 5
                            
                                |
94 | 75, 82, 93 | 3eqtrd 2509 |
. . . 4
                  
                      |
95 | | oveq2 6316 |
. . . . . . . . 9
       |
96 | | oveq1 6315 |
. . . . . . . . . 10
  BernPoly     BernPoly      |
97 | | oveq2 6316 |
. . . . . . . . . . 11
 
     |
98 | 97 | oveq1d 6323 |
. . . . . . . . . 10
           |
99 | 96, 98 | oveq12d 6326 |
. . . . . . . . 9
   BernPoly
          BernPoly 
         |
100 | 95, 99 | oveq12d 6326 |
. . . . . . . 8
      BernPoly               BernPoly
           |
101 | 78, 35, 100 | fsum1p 13891 |
. . . . . . 7
              BernPoly
               BernPoly 
        
              BernPoly             |
102 | | bpoly0 14180 |
. . . . . . . . . . 11
    BernPoly      |
103 | 5, 102 | syl 17 |
. . . . . . . . . 10
  BernPoly      |
104 | 103 | oveq1d 6323 |
. . . . . . . . 9
   BernPoly 
               |
105 | 104 | oveq2d 6324 |
. . . . . . . 8
      BernPoly
                     |
106 | 105 | oveq1d 6323 |
. . . . . . 7
       BernPoly 
              
        BernPoly 
                          
        BernPoly 
           |
107 | 101, 106 | eqtrd 2505 |
. . . . . 6
              BernPoly
                                   BernPoly
            |
108 | | oveq1 6315 |
. . . . . . . . . 10
  BernPoly   BernPoly    |
109 | 108, 98 | oveq12d 6326 |
. . . . . . . . 9
   BernPoly
        BernPoly         |
110 | 95, 109 | oveq12d 6326 |
. . . . . . . 8
      BernPoly             BernPoly          |
111 | 78, 41, 110 | fsum1p 13891 |
. . . . . . 7
              BernPoly
             BernPoly        
              BernPoly           |
112 | | bpoly0 14180 |
. . . . . . . . . . 11
  BernPoly    |
113 | 3, 112 | syl 17 |
. . . . . . . . . 10
  BernPoly    |
114 | 113 | oveq1d 6323 |
. . . . . . . . 9
   BernPoly               |
115 | 114 | oveq2d 6324 |
. . . . . . . 8
      BernPoly
                   |
116 | 115 | oveq1d 6323 |
. . . . . . 7
       BernPoly              
        BernPoly                          
        BernPoly           |
117 | 111, 116 | eqtrd 2505 |
. . . . . 6
              BernPoly
                                 BernPoly
          |
118 | 107, 117 | oveq12d 6326 |
. . . . 5
               BernPoly
                      BernPoly
                          
        BernPoly 
                          
        BernPoly            |
119 | | 0z 10972 |
. . . . . . . . 9
 |
120 | | bccl 12545 |
. . . . . . . . 9
 
     |
121 | 2, 119, 120 | sylancl 675 |
. . . . . . . 8
     |
122 | 121 | nn0cnd 10951 |
. . . . . . 7
     |
123 | 21 | subid1d 9994 |
. . . . . . . . . . 11
     |
124 | 123, 1 | eqeltrd 2549 |
. . . . . . . . . 10
     |
125 | 124 | peano2nnd 10648 |
. . . . . . . . 9
       |
126 | 125 | nnrecred 10677 |
. . . . . . . 8
         |
127 | 126 | recnd 9687 |
. . . . . . 7
         |
128 | 122, 127 | mulcld 9681 |
. . . . . 6
             |
129 | | fzfid 12224 |
. . . . . . 7
      
    |
130 | | fzp1ss 11873 |
. . . . . . . . . 10
                 |
131 | 119, 130 | ax-mp 5 |
. . . . . . . . 9
           
   |
132 | 131 | sseli 3414 |
. . . . . . . 8
            
    |
133 | 132, 35 | sylan2 482 |
. . . . . . 7
 
     
        BernPoly            |
134 | 129, 133 | fsumcl 13876 |
. . . . . 6
                BernPoly
           |
135 | 132, 41 | sylan2 482 |
. . . . . . 7
 
     
        BernPoly          |
136 | 129, 135 | fsumcl 13876 |
. . . . . 6
                BernPoly
         |
137 | 128, 134,
136 | pnpcand 10042 |
. . . . 5
                            BernPoly
                                    BernPoly
                         BernPoly
                        BernPoly
          |
138 | | 1zzd 10992 |
. . . . . . . 8
   |
139 | | 0zd 10973 |
. . . . . . . 8
   |
140 | 1 | nnzd 11062 |
. . . . . . . . 9
   |
141 | | 2z 10993 |
. . . . . . . . 9
 |
142 | | zsubcl 11003 |
. . . . . . . . 9
 
     |
143 | 140, 141,
142 | sylancl 675 |
. . . . . . . 8
     |
144 | | fzssp1 11867 |
. . . . . . . . . . 11
               |
145 | | 2m1e1 10746 |
. . . . . . . . . . . . . 14
   |
146 | 145 | oveq2i 6319 |
. . . . . . . . . . . . 13
       |
147 | | 2cnd 10704 |
. . . . . . . . . . . . . 14
   |
148 | 21, 147, 83 | subsubd 10033 |
. . . . . . . . . . . . 13
           |
149 | 146, 148 | syl5reqr 2520 |
. . . . . . . . . . . 12
         |
150 | 149 | oveq2d 6324 |
. . . . . . . . . . 11
                 |
151 | 144, 150 | syl5sseq 3466 |
. . . . . . . . . 10
    
 
        |
152 | 151 | sselda 3418 |
. . . . . . . . 9
 
   
      
    |
153 | 152, 72 | syldan 478 |
. . . . . . . 8
 
   
             |
154 | | oveq2 6316 |
. . . . . . . . 9
           |
155 | | oveq2 6316 |
. . . . . . . . 9
               |
156 | 154, 155 | oveq12d 6326 |
. . . . . . . 8
                         |
157 | 138, 139,
143, 153, 156 | fsumshft 13918 |
. . . . . . 7
 
                                         |
158 | 149 | oveq2d 6324 |
. . . . . . . 8
                     |
159 | 158 | sumeq1d 13844 |
. . . . . . 7
                                                 |
160 | 157, 159 | eqtrd 2505 |
. . . . . 6
 
                                       |
161 | | 0p1e1 10743 |
. . . . . . . . . 10
   |
162 | 161 | oveq1i 6318 |
. . . . . . . . 9
           
   |
163 | 162 | eleq2i 2541 |
. . . . . . . 8
        
   
    |
164 | | fzssp1 11867 |
. . . . . . . . . . . . . 14
               |
165 | 24 | oveq2d 6324 |
. . . . . . . . . . . . . 14
               |
166 | 164, 165 | syl5sseq 3466 |
. . . . . . . . . . . . 13
    
 
      |
167 | 166 | sselda 3418 |
. . . . . . . . . . . 12
 
   
         |
168 | | bcm1k 12538 |
. . . . . . . . . . . 12
                     |
169 | 167, 168 | syl 17 |
. . . . . . . . . . 11
 
   
                   |
170 | 1 | adantr 472 |
. . . . . . . . . . . . . . 15
 
   
     |
171 | 170 | nncnd 10647 |
. . . . . . . . . . . . . 14
 
   
     |
172 | | elfznn 11854 |
. . . . . . . . . . . . . . . 16
         |
173 | 172 | adantl 473 |
. . . . . . . . . . . . . . 15
 
   
     |
174 | 173 | nncnd 10647 |
. . . . . . . . . . . . . 14
 
   
     |
175 | | 1cnd 9677 |
. . . . . . . . . . . . . 14
 
   
     |
176 | 171, 174,
175 | subsubd 10033 |
. . . . . . . . . . . . 13
 
   
   
         |
177 | 176 | oveq1d 6323 |
. . . . . . . . . . . 12
 
   
                 |
178 | 177 | oveq2d 6324 |
. . . . . . . . . . 11
 
   
                             |
179 | 169, 178 | eqtrd 2505 |
. . . . . . . . . 10
 
   
                   |
180 | | bpolydiflem.3 |
. . . . . . . . . . . 12
 
   
     BernPoly
    BernPoly             |
181 | 180 | oveq1d 6323 |
. . . . . . . . . . 11
 
   
      BernPoly 
   BernPoly                        |
182 | 163, 132 | sylbir 218 |
. . . . . . . . . . . . 13
          
    |
183 | 182, 19 | sylan2 482 |
. . . . . . . . . . . 12
 
   
    BernPoly      |
184 | 182, 39 | sylan2 482 |
. . . . . . . . . . . 12
 
   
    BernPoly    |
185 | 182, 32 | sylan2 482 |
. . . . . . . . . . . 12
 
   
         |
186 | 182, 33 | sylan2 482 |
. . . . . . . . . . . 12
 
   
         |
187 | 183, 184,
185, 186 | divsubdird 10444 |
. . . . . . . . . . 11
 
   
      BernPoly 
   BernPoly           BernPoly 
         BernPoly          |
188 | 3 | adantr 472 |
. . . . . . . . . . . . 13
 
   
     |
189 | | nnm1nn0 10935 |
. . . . . . . . . . . . . 14
     |
190 | 173, 189 | syl 17 |
. . . . . . . . . . . . 13
 
   
       |
191 | 188, 190 | expcld 12454 |
. . . . . . . . . . . 12
 
   
           |
192 | 174, 191,
185, 186 | div23d 10442 |
. . . . . . . . . . 11
 
   
                                 |
193 | 181, 187,
192 | 3eqtr3d 2513 |
. . . . . . . . . 10
 
   
      BernPoly 
         BernPoly                        |
194 | 179, 193 | oveq12d 6326 |
. . . . . . . . 9
 
   
         BernPoly           BernPoly                                       |
195 | 182, 16 | sylan2 482 |
. . . . . . . . . 10
 
   
       |
196 | 183, 185,
186 | divcld 10405 |
. . . . . . . . . 10
 
   
     BernPoly
          |
197 | 184, 185,
186 | divcld 10405 |
. . . . . . . . . 10
 
   
     BernPoly
        |
198 | 195, 196,
197 | subdid 10095 |
. . . . . . . . 9
 
   
         BernPoly           BernPoly               BernPoly
              BernPoly           |
199 | 170 | nnnn0d 10949 |
. . . . . . . . . . . . 13
 
   
     |
200 | 190 | nn0zd 11061 |
. . . . . . . . . . . . 13
 
   
       |
201 | | bccl 12545 |
. . . . . . . . . . . . 13
           |
202 | 199, 200,
201 | syl2anc 673 |
. . . . . . . . . . . 12
 
   
         |
203 | 202 | nn0cnd 10951 |
. . . . . . . . . . 11
 
   
         |
204 | 173 | nnne0d 10676 |
. . . . . . . . . . . 12
 
   
     |
205 | 185, 174,
204 | divcld 10405 |
. . . . . . . . . . 11
 
   
           |
206 | 174, 185,
186 | divcld 10405 |
. . . . . . . . . . . 12
 
   
           |
207 | 206, 191 | mulcld 9681 |
. . . . . . . . . . 11
 
   
                   |
208 | 203, 205,
207 | mulassd 9684 |
. . . . . . . . . 10
 
   
                                                             |
209 | 185, 174,
186, 204 | divcan6d 10424 |
. . . . . . . . . . . . 13
 
   
                   |
210 | 209 | oveq1d 6323 |
. . . . . . . . . . . 12
 
   
                                   |
211 | 205, 206,
191 | mulassd 9684 |
. . . . . . . . . . . 12
 
   
                                                 |
212 | 191 | mulid2d 9679 |
. . . . . . . . . . . 12
 
   
                   |
213 | 210, 211,
212 | 3eqtr3d 2513 |
. . . . . . . . . . 11
 
   
                                 |
214 | 213 | oveq2d 6324 |
. . . . . . . . . 10
 
   
                                             |
215 | 208, 214 | eqtrd 2505 |
. . . . . . . . 9
 
   
                                             |
216 | 194, 198,
215 | 3eqtr3d 2513 |
. . . . . . . 8
 
   
         BernPoly
              BernPoly                       |
217 | 163, 216 | sylan2b 483 |
. . . . . . 7
 
     
         BernPoly
              BernPoly                       |
218 | 217 | sumeq2dv 13846 |
. . . . . 6
                 BernPoly 
             BernPoly                                 |
219 | 129, 133,
135 | fsumsub 13926 |
. . . . . 6
                 BernPoly 
             BernPoly                         BernPoly
                        BernPoly
          |
220 | 160, 218,
219 | 3eqtr2rd 2512 |
. . . . 5
                 BernPoly
                        BernPoly
            
             |
221 | 118, 137,
220 | 3eqtrd 2509 |
. . . 4
               BernPoly
                      BernPoly
            
             |
222 | 94, 221 | oveq12d 6326 |
. . 3
               
            BernPoly                       BernPoly                                         
              |
223 | | fzfid 12224 |
. . . . 5
    
    |
224 | 223, 153 | fsumcl 13876 |
. . . 4
 
                 |
225 | 3, 77 | expcld 12454 |
. . . . 5
    
    |
226 | 21, 225 | mulcld 9681 |
. . . 4
           |
227 | 224, 226 | pncan2d 10007 |
. . 3
       
                        
                      |
228 | 222, 227 | eqtrd 2505 |
. 2
               
            BernPoly                       BernPoly                    |
229 | 10, 43, 228 | 3eqtrd 2509 |
1
   BernPoly 
   BernPoly             |