Step | Hyp | Ref
| Expression |
1 | | bpolydiflem.1 |
. . . . 5
|
2 | 1 | nnnn0d 11351 |
. . . 4
|
3 | | bpolydiflem.2 |
. . . . 5
|
4 | | peano2cn 10208 |
. . . . 5
|
5 | 3, 4 | syl 17 |
. . . 4
|
6 | | bpolyval 14780 |
. . . 4
BernPoly
BernPoly
|
7 | 2, 5, 6 | syl2anc 693 |
. . 3
BernPoly
BernPoly |
8 | | bpolyval 14780 |
. . . 4
BernPoly
BernPoly |
9 | 2, 3, 8 | syl2anc 693 |
. . 3
BernPoly
BernPoly |
10 | 7, 9 | oveq12d 6668 |
. 2
BernPoly
BernPoly BernPoly BernPoly |
11 | 5, 2 | expcld 13008 |
. . 3
|
12 | | fzfid 12772 |
. . . 4
|
13 | | elfzelz 12342 |
. . . . . . 7
|
14 | | bccl 13109 |
. . . . . . 7
|
15 | 2, 13, 14 | syl2an 494 |
. . . . . 6
|
16 | 15 | nn0cnd 11353 |
. . . . 5
|
17 | | elfznn0 12433 |
. . . . . . 7
|
18 | | bpolycl 14783 |
. . . . . . 7
BernPoly
|
19 | 17, 5, 18 | syl2anr 495 |
. . . . . 6
BernPoly |
20 | | fzssp1 12384 |
. . . . . . . . . . 11
|
21 | 1 | nncnd 11036 |
. . . . . . . . . . . . 13
|
22 | | ax-1cn 9994 |
. . . . . . . . . . . . 13
|
23 | | npcan 10290 |
. . . . . . . . . . . . 13
|
24 | 21, 22, 23 | sylancl 694 |
. . . . . . . . . . . 12
|
25 | 24 | oveq2d 6666 |
. . . . . . . . . . 11
|
26 | 20, 25 | syl5sseq 3653 |
. . . . . . . . . 10
|
27 | 26 | sselda 3603 |
. . . . . . . . 9
|
28 | | fznn0sub 12373 |
. . . . . . . . 9
|
29 | 27, 28 | syl 17 |
. . . . . . . 8
|
30 | | nn0p1nn 11332 |
. . . . . . . 8
|
31 | 29, 30 | syl 17 |
. . . . . . 7
|
32 | 31 | nncnd 11036 |
. . . . . 6
|
33 | 31 | nnne0d 11065 |
. . . . . 6
|
34 | 19, 32, 33 | divcld 10801 |
. . . . 5
BernPoly
|
35 | 16, 34 | mulcld 10060 |
. . . 4
BernPoly |
36 | 12, 35 | fsumcl 14464 |
. . 3
BernPoly
|
37 | 3, 2 | expcld 13008 |
. . 3
|
38 | | bpolycl 14783 |
. . . . . . 7
BernPoly |
39 | 17, 3, 38 | syl2anr 495 |
. . . . . 6
BernPoly |
40 | 39, 32, 33 | divcld 10801 |
. . . . 5
BernPoly
|
41 | 16, 40 | mulcld 10060 |
. . . 4
BernPoly |
42 | 12, 41 | fsumcl 14464 |
. . 3
BernPoly
|
43 | 11, 36, 37, 42 | sub4d 10441 |
. 2
BernPoly BernPoly BernPoly
BernPoly
|
44 | | addcom 10222 |
. . . . . . . . . . 11
|
45 | 3, 22, 44 | sylancl 694 |
. . . . . . . . . 10
|
46 | 45 | oveq1d 6665 |
. . . . . . . . 9
|
47 | | binom1p 14563 |
. . . . . . . . . 10
|
48 | 3, 2, 47 | syl2anc 693 |
. . . . . . . . 9
|
49 | 46, 48 | eqtrd 2656 |
. . . . . . . 8
|
50 | | nn0uz 11722 |
. . . . . . . . . 10
|
51 | 2, 50 | syl6eleq 2711 |
. . . . . . . . 9
|
52 | | bccl2 13110 |
. . . . . . . . . . . 12
|
53 | 52 | adantl 482 |
. . . . . . . . . . 11
|
54 | 53 | nncnd 11036 |
. . . . . . . . . 10
|
55 | | elfznn0 12433 |
. . . . . . . . . . 11
|
56 | | expcl 12878 |
. . . . . . . . . . 11
|
57 | 3, 55, 56 | syl2an 494 |
. . . . . . . . . 10
|
58 | 54, 57 | mulcld 10060 |
. . . . . . . . 9
|
59 | | oveq2 6658 |
. . . . . . . . . 10
|
60 | | oveq2 6658 |
. . . . . . . . . 10
|
61 | 59, 60 | oveq12d 6668 |
. . . . . . . . 9
|
62 | 51, 58, 61 | fsumm1 14480 |
. . . . . . . 8
|
63 | | bcnn 13099 |
. . . . . . . . . . . 12
|
64 | 2, 63 | syl 17 |
. . . . . . . . . . 11
|
65 | 64 | oveq1d 6665 |
. . . . . . . . . 10
|
66 | 37 | mulid2d 10058 |
. . . . . . . . . 10
|
67 | 65, 66 | eqtrd 2656 |
. . . . . . . . 9
|
68 | 67 | oveq2d 6666 |
. . . . . . . 8
|
69 | 49, 62, 68 | 3eqtrd 2660 |
. . . . . . 7
|
70 | 69 | oveq1d 6665 |
. . . . . 6
|
71 | 26 | sselda 3603 |
. . . . . . . . 9
|
72 | 71, 58 | syldan 487 |
. . . . . . . 8
|
73 | 12, 72 | fsumcl 14464 |
. . . . . . 7
|
74 | 73, 37 | pncand 10393 |
. . . . . 6
|
75 | 70, 74 | eqtrd 2656 |
. . . . 5
|
76 | | nnm1nn0 11334 |
. . . . . . . 8
|
77 | 1, 76 | syl 17 |
. . . . . . 7
|
78 | 77, 50 | syl6eleq 2711 |
. . . . . 6
|
79 | | oveq2 6658 |
. . . . . . 7
|
80 | | oveq2 6658 |
. . . . . . 7
|
81 | 79, 80 | oveq12d 6668 |
. . . . . 6
|
82 | 78, 72, 81 | fsumm1 14480 |
. . . . 5
|
83 | | 1cnd 10056 |
. . . . . . . . . 10
|
84 | 21, 83, 83 | subsub4d 10423 |
. . . . . . . . 9
|
85 | | df-2 11079 |
. . . . . . . . . 10
|
86 | 85 | oveq2i 6661 |
. . . . . . . . 9
|
87 | 84, 86 | syl6eqr 2674 |
. . . . . . . 8
|
88 | 87 | oveq2d 6666 |
. . . . . . 7
|
89 | 88 | sumeq1d 14431 |
. . . . . 6
|
90 | | bcnm1 13114 |
. . . . . . . 8
|
91 | 2, 90 | syl 17 |
. . . . . . 7
|
92 | 91 | oveq1d 6665 |
. . . . . 6
|
93 | 89, 92 | oveq12d 6668 |
. . . . 5
|
94 | 75, 82, 93 | 3eqtrd 2660 |
. . . 4
|
95 | | oveq2 6658 |
. . . . . . . . 9
|
96 | | oveq1 6657 |
. . . . . . . . . 10
BernPoly BernPoly |
97 | | oveq2 6658 |
. . . . . . . . . . 11
|
98 | 97 | oveq1d 6665 |
. . . . . . . . . 10
|
99 | 96, 98 | oveq12d 6668 |
. . . . . . . . 9
BernPoly
BernPoly
|
100 | 95, 99 | oveq12d 6668 |
. . . . . . . 8
BernPoly BernPoly
|
101 | 78, 35, 100 | fsum1p 14482 |
. . . . . . 7
BernPoly
BernPoly
BernPoly |
102 | | bpoly0 14781 |
. . . . . . . . . . 11
BernPoly |
103 | 5, 102 | syl 17 |
. . . . . . . . . 10
BernPoly |
104 | 103 | oveq1d 6665 |
. . . . . . . . 9
BernPoly
|
105 | 104 | oveq2d 6666 |
. . . . . . . 8
BernPoly
|
106 | 105 | oveq1d 6665 |
. . . . . . 7
BernPoly
BernPoly
BernPoly
|
107 | 101, 106 | eqtrd 2656 |
. . . . . 6
BernPoly
BernPoly
|
108 | | oveq1 6657 |
. . . . . . . . . 10
BernPoly BernPoly |
109 | 108, 98 | oveq12d 6668 |
. . . . . . . . 9
BernPoly
BernPoly |
110 | 95, 109 | oveq12d 6668 |
. . . . . . . 8
BernPoly BernPoly |
111 | 78, 41, 110 | fsum1p 14482 |
. . . . . . 7
BernPoly
BernPoly
BernPoly |
112 | | bpoly0 14781 |
. . . . . . . . . . 11
BernPoly |
113 | 3, 112 | syl 17 |
. . . . . . . . . 10
BernPoly |
114 | 113 | oveq1d 6665 |
. . . . . . . . 9
BernPoly |
115 | 114 | oveq2d 6666 |
. . . . . . . 8
BernPoly
|
116 | 115 | oveq1d 6665 |
. . . . . . 7
BernPoly
BernPoly
BernPoly |
117 | 111, 116 | eqtrd 2656 |
. . . . . 6
BernPoly
BernPoly
|
118 | 107, 117 | oveq12d 6668 |
. . . . 5
BernPoly
BernPoly
BernPoly
BernPoly |
119 | | 0z 11388 |
. . . . . . . . 9
|
120 | | bccl 13109 |
. . . . . . . . 9
|
121 | 2, 119, 120 | sylancl 694 |
. . . . . . . 8
|
122 | 121 | nn0cnd 11353 |
. . . . . . 7
|
123 | 21 | subid1d 10381 |
. . . . . . . . . . 11
|
124 | 123, 1 | eqeltrd 2701 |
. . . . . . . . . 10
|
125 | 124 | peano2nnd 11037 |
. . . . . . . . 9
|
126 | 125 | nnrecred 11066 |
. . . . . . . 8
|
127 | 126 | recnd 10068 |
. . . . . . 7
|
128 | 122, 127 | mulcld 10060 |
. . . . . 6
|
129 | | fzfid 12772 |
. . . . . . 7
|
130 | | fzp1ss 12392 |
. . . . . . . . . 10
|
131 | 119, 130 | ax-mp 5 |
. . . . . . . . 9
|
132 | 131 | sseli 3599 |
. . . . . . . 8
|
133 | 132, 35 | sylan2 491 |
. . . . . . 7
BernPoly |
134 | 129, 133 | fsumcl 14464 |
. . . . . 6
BernPoly
|
135 | 132, 41 | sylan2 491 |
. . . . . . 7
BernPoly |
136 | 129, 135 | fsumcl 14464 |
. . . . . 6
BernPoly
|
137 | 128, 134,
136 | pnpcand 10429 |
. . . . 5
BernPoly
BernPoly
BernPoly
BernPoly
|
138 | | 1zzd 11408 |
. . . . . . . 8
|
139 | | 0zd 11389 |
. . . . . . . 8
|
140 | 1 | nnzd 11481 |
. . . . . . . . 9
|
141 | | 2z 11409 |
. . . . . . . . 9
|
142 | | zsubcl 11419 |
. . . . . . . . 9
|
143 | 140, 141,
142 | sylancl 694 |
. . . . . . . 8
|
144 | | fzssp1 12384 |
. . . . . . . . . . 11
|
145 | | 2m1e1 11135 |
. . . . . . . . . . . . . 14
|
146 | 145 | oveq2i 6661 |
. . . . . . . . . . . . 13
|
147 | | 2cnd 11093 |
. . . . . . . . . . . . . 14
|
148 | 21, 147, 83 | subsubd 10420 |
. . . . . . . . . . . . 13
|
149 | 146, 148 | syl5reqr 2671 |
. . . . . . . . . . . 12
|
150 | 149 | oveq2d 6666 |
. . . . . . . . . . 11
|
151 | 144, 150 | syl5sseq 3653 |
. . . . . . . . . 10
|
152 | 151 | sselda 3603 |
. . . . . . . . 9
|
153 | 152, 72 | syldan 487 |
. . . . . . . 8
|
154 | | oveq2 6658 |
. . . . . . . . 9
|
155 | | oveq2 6658 |
. . . . . . . . 9
|
156 | 154, 155 | oveq12d 6668 |
. . . . . . . 8
|
157 | 138, 139,
143, 153, 156 | fsumshft 14512 |
. . . . . . 7
|
158 | 149 | oveq2d 6666 |
. . . . . . . 8
|
159 | 158 | sumeq1d 14431 |
. . . . . . 7
|
160 | 157, 159 | eqtrd 2656 |
. . . . . 6
|
161 | | 0p1e1 11132 |
. . . . . . . . . 10
|
162 | 161 | oveq1i 6660 |
. . . . . . . . 9
|
163 | 162 | eleq2i 2693 |
. . . . . . . 8
|
164 | | fzssp1 12384 |
. . . . . . . . . . . . . 14
|
165 | 24 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
166 | 164, 165 | syl5sseq 3653 |
. . . . . . . . . . . . 13
|
167 | 166 | sselda 3603 |
. . . . . . . . . . . 12
|
168 | | bcm1k 13102 |
. . . . . . . . . . . 12
|
169 | 167, 168 | syl 17 |
. . . . . . . . . . 11
|
170 | 1 | adantr 481 |
. . . . . . . . . . . . . . 15
|
171 | 170 | nncnd 11036 |
. . . . . . . . . . . . . 14
|
172 | | elfznn 12370 |
. . . . . . . . . . . . . . . 16
|
173 | 172 | adantl 482 |
. . . . . . . . . . . . . . 15
|
174 | 173 | nncnd 11036 |
. . . . . . . . . . . . . 14
|
175 | | 1cnd 10056 |
. . . . . . . . . . . . . 14
|
176 | 171, 174,
175 | subsubd 10420 |
. . . . . . . . . . . . 13
|
177 | 176 | oveq1d 6665 |
. . . . . . . . . . . 12
|
178 | 177 | oveq2d 6666 |
. . . . . . . . . . 11
|
179 | 169, 178 | eqtrd 2656 |
. . . . . . . . . 10
|
180 | | bpolydiflem.3 |
. . . . . . . . . . . 12
BernPoly
BernPoly |
181 | 180 | oveq1d 6665 |
. . . . . . . . . . 11
BernPoly
BernPoly |
182 | 163, 132 | sylbir 225 |
. . . . . . . . . . . . 13
|
183 | 182, 19 | sylan2 491 |
. . . . . . . . . . . 12
BernPoly |
184 | 182, 39 | sylan2 491 |
. . . . . . . . . . . 12
BernPoly |
185 | 182, 32 | sylan2 491 |
. . . . . . . . . . . 12
|
186 | 182, 33 | sylan2 491 |
. . . . . . . . . . . 12
|
187 | 183, 184,
185, 186 | divsubdird 10840 |
. . . . . . . . . . 11
BernPoly
BernPoly BernPoly
BernPoly |
188 | 3 | adantr 481 |
. . . . . . . . . . . . 13
|
189 | | nnm1nn0 11334 |
. . . . . . . . . . . . . 14
|
190 | 173, 189 | syl 17 |
. . . . . . . . . . . . 13
|
191 | 188, 190 | expcld 13008 |
. . . . . . . . . . . 12
|
192 | 174, 191,
185, 186 | div23d 10838 |
. . . . . . . . . . 11
|
193 | 181, 187,
192 | 3eqtr3d 2664 |
. . . . . . . . . 10
BernPoly
BernPoly |
194 | 179, 193 | oveq12d 6668 |
. . . . . . . . 9
BernPoly BernPoly |
195 | 182, 16 | sylan2 491 |
. . . . . . . . . 10
|
196 | 183, 185,
186 | divcld 10801 |
. . . . . . . . . 10
BernPoly
|
197 | 184, 185,
186 | divcld 10801 |
. . . . . . . . . 10
BernPoly
|
198 | 195, 196,
197 | subdid 10486 |
. . . . . . . . 9
BernPoly BernPoly BernPoly
BernPoly |
199 | 170 | nnnn0d 11351 |
. . . . . . . . . . . . 13
|
200 | 190 | nn0zd 11480 |
. . . . . . . . . . . . 13
|
201 | | bccl 13109 |
. . . . . . . . . . . . 13
|
202 | 199, 200,
201 | syl2anc 693 |
. . . . . . . . . . . 12
|
203 | 202 | nn0cnd 11353 |
. . . . . . . . . . 11
|
204 | 173 | nnne0d 11065 |
. . . . . . . . . . . 12
|
205 | 185, 174,
204 | divcld 10801 |
. . . . . . . . . . 11
|
206 | 174, 185,
186 | divcld 10801 |
. . . . . . . . . . . 12
|
207 | 206, 191 | mulcld 10060 |
. . . . . . . . . . 11
|
208 | 203, 205,
207 | mulassd 10063 |
. . . . . . . . . 10
|
209 | 185, 174,
186, 204 | divcan6d 10820 |
. . . . . . . . . . . . 13
|
210 | 209 | oveq1d 6665 |
. . . . . . . . . . . 12
|
211 | 205, 206,
191 | mulassd 10063 |
. . . . . . . . . . . 12
|
212 | 191 | mulid2d 10058 |
. . . . . . . . . . . 12
|
213 | 210, 211,
212 | 3eqtr3d 2664 |
. . . . . . . . . . 11
|
214 | 213 | oveq2d 6666 |
. . . . . . . . . 10
|
215 | 208, 214 | eqtrd 2656 |
. . . . . . . . 9
|
216 | 194, 198,
215 | 3eqtr3d 2664 |
. . . . . . . 8
BernPoly
BernPoly |
217 | 163, 216 | sylan2b 492 |
. . . . . . 7
BernPoly
BernPoly |
218 | 217 | sumeq2dv 14433 |
. . . . . 6
BernPoly
BernPoly |
219 | 129, 133,
135 | fsumsub 14520 |
. . . . . 6
BernPoly
BernPoly BernPoly
BernPoly
|
220 | 160, 218,
219 | 3eqtr2rd 2663 |
. . . . 5
BernPoly
BernPoly
|
221 | 118, 137,
220 | 3eqtrd 2660 |
. . . 4
BernPoly
BernPoly
|
222 | 94, 221 | oveq12d 6668 |
. . 3
BernPoly BernPoly
|
223 | | fzfid 12772 |
. . . . 5
|
224 | 223, 153 | fsumcl 14464 |
. . . 4
|
225 | 3, 77 | expcld 13008 |
. . . . 5
|
226 | 21, 225 | mulcld 10060 |
. . . 4
|
227 | 224, 226 | pncan2d 10394 |
. . 3
|
228 | 222, 227 | eqtrd 2656 |
. 2
BernPoly BernPoly |
229 | 10, 43, 228 | 3eqtrd 2660 |
1
BernPoly
BernPoly |