Metamath Proof Explorer


Theorem bpoly3

Description: The Bernoulli polynomials at three. (Contributed by Scott Fenton, 8-Jul-2015)

Ref Expression
Assertion bpoly3 X 3 BernPoly X = X 3 - 3 2 X 2 + 1 2 X

Proof

Step Hyp Ref Expression
1 3nn0 3 0
2 bpolyval 3 0 X 3 BernPoly X = X 3 k = 0 3 1 ( 3 k) k BernPoly X 3 - k + 1
3 1 2 mpan X 3 BernPoly X = X 3 k = 0 3 1 ( 3 k) k BernPoly X 3 - k + 1
4 3m1e2 3 1 = 2
5 df-2 2 = 1 + 1
6 4 5 eqtri 3 1 = 1 + 1
7 6 oveq2i 0 3 1 = 0 1 + 1
8 7 sumeq1i k = 0 3 1 ( 3 k) k BernPoly X 3 - k + 1 = k = 0 1 + 1 ( 3 k) k BernPoly X 3 - k + 1
9 1eluzge0 1 0
10 9 a1i X 1 0
11 0z 0
12 fzpr 0 0 0 + 1 = 0 0 + 1
13 11 12 ax-mp 0 0 + 1 = 0 0 + 1
14 0p1e1 0 + 1 = 1
15 14 oveq2i 0 0 + 1 = 0 1
16 14 preq2i 0 0 + 1 = 0 1
17 13 15 16 3eqtr3ri 0 1 = 0 1
18 5 sneqi 2 = 1 + 1
19 17 18 uneq12i 0 1 2 = 0 1 1 + 1
20 df-tp 0 1 2 = 0 1 2
21 fzsuc 1 0 0 1 + 1 = 0 1 1 + 1
22 9 21 ax-mp 0 1 + 1 = 0 1 1 + 1
23 19 20 22 3eqtr4ri 0 1 + 1 = 0 1 2
24 23 eleq2i k 0 1 + 1 k 0 1 2
25 vex k V
26 25 eltp k 0 1 2 k = 0 k = 1 k = 2
27 24 26 bitri k 0 1 + 1 k = 0 k = 1 k = 2
28 oveq2 k = 0 ( 3 k) = ( 3 0 )
29 bcn0 3 0 ( 3 0 ) = 1
30 1 29 ax-mp ( 3 0 ) = 1
31 28 30 eqtrdi k = 0 ( 3 k) = 1
32 oveq1 k = 0 k BernPoly X = 0 BernPoly X
33 oveq2 k = 0 3 k = 3 0
34 33 oveq1d k = 0 3 - k + 1 = 3 - 0 + 1
35 3cn 3
36 35 subid1i 3 0 = 3
37 36 oveq1i 3 - 0 + 1 = 3 + 1
38 df-4 4 = 3 + 1
39 37 38 eqtr4i 3 - 0 + 1 = 4
40 34 39 eqtrdi k = 0 3 - k + 1 = 4
41 32 40 oveq12d k = 0 k BernPoly X 3 - k + 1 = 0 BernPoly X 4
42 31 41 oveq12d k = 0 ( 3 k) k BernPoly X 3 - k + 1 = 1 0 BernPoly X 4
43 bpoly0 X 0 BernPoly X = 1
44 43 oveq1d X 0 BernPoly X 4 = 1 4
45 44 oveq2d X 1 0 BernPoly X 4 = 1 1 4
46 4cn 4
47 4ne0 4 0
48 46 47 reccli 1 4
49 48 mulid2i 1 1 4 = 1 4
50 45 49 eqtrdi X 1 0 BernPoly X 4 = 1 4
51 42 50 sylan9eqr X k = 0 ( 3 k) k BernPoly X 3 - k + 1 = 1 4
52 51 48 eqeltrdi X k = 0 ( 3 k) k BernPoly X 3 - k + 1
53 oveq2 k = 1 ( 3 k) = ( 3 1 )
54 bcn1 3 0 ( 3 1 ) = 3
55 1 54 ax-mp ( 3 1 ) = 3
56 53 55 eqtrdi k = 1 ( 3 k) = 3
57 oveq1 k = 1 k BernPoly X = 1 BernPoly X
58 oveq2 k = 1 3 k = 3 1
59 58 oveq1d k = 1 3 - k + 1 = 3 - 1 + 1
60 ax-1cn 1
61 npcan 3 1 3 - 1 + 1 = 3
62 35 60 61 mp2an 3 - 1 + 1 = 3
63 59 62 eqtrdi k = 1 3 - k + 1 = 3
64 57 63 oveq12d k = 1 k BernPoly X 3 - k + 1 = 1 BernPoly X 3
65 56 64 oveq12d k = 1 ( 3 k) k BernPoly X 3 - k + 1 = 3 1 BernPoly X 3
66 bpoly1 X 1 BernPoly X = X 1 2
67 66 oveq1d X 1 BernPoly X 3 = X 1 2 3
68 67 oveq2d X 3 1 BernPoly X 3 = 3 X 1 2 3
69 halfcn 1 2
70 subcl X 1 2 X 1 2
71 69 70 mpan2 X X 1 2
72 3ne0 3 0
73 divcan2 X 1 2 3 3 0 3 X 1 2 3 = X 1 2
74 35 72 73 mp3an23 X 1 2 3 X 1 2 3 = X 1 2
75 71 74 syl X 3 X 1 2 3 = X 1 2
76 68 75 eqtrd X 3 1 BernPoly X 3 = X 1 2
77 65 76 sylan9eqr X k = 1 ( 3 k) k BernPoly X 3 - k + 1 = X 1 2
78 71 adantr X k = 1 X 1 2
79 77 78 eqeltrd X k = 1 ( 3 k) k BernPoly X 3 - k + 1
80 oveq2 k = 2 ( 3 k) = ( 3 2 )
81 bcn2 3 0 ( 3 2 ) = 3 3 1 2
82 1 81 ax-mp ( 3 2 ) = 3 3 1 2
83 4 oveq2i 3 3 1 = 3 2
84 83 oveq1i 3 3 1 2 = 3 2 2
85 2cn 2
86 2ne0 2 0
87 35 85 86 divcan4i 3 2 2 = 3
88 84 87 eqtri 3 3 1 2 = 3
89 82 88 eqtri ( 3 2 ) = 3
90 80 89 eqtrdi k = 2 ( 3 k) = 3
91 oveq1 k = 2 k BernPoly X = 2 BernPoly X
92 oveq2 k = 2 3 k = 3 2
93 92 oveq1d k = 2 3 - k + 1 = 3 - 2 + 1
94 2p1e3 2 + 1 = 3
95 35 85 60 94 subaddrii 3 2 = 1
96 95 oveq1i 3 - 2 + 1 = 1 + 1
97 96 5 eqtr4i 3 - 2 + 1 = 2
98 93 97 eqtrdi k = 2 3 - k + 1 = 2
99 91 98 oveq12d k = 2 k BernPoly X 3 - k + 1 = 2 BernPoly X 2
100 90 99 oveq12d k = 2 ( 3 k) k BernPoly X 3 - k + 1 = 3 2 BernPoly X 2
101 2nn0 2 0
102 bpolycl 2 0 X 2 BernPoly X
103 101 102 mpan X 2 BernPoly X
104 2cnne0 2 2 0
105 div12 3 2 BernPoly X 2 2 0 3 2 BernPoly X 2 = 2 BernPoly X 3 2
106 35 104 105 mp3an13 2 BernPoly X 3 2 BernPoly X 2 = 2 BernPoly X 3 2
107 103 106 syl X 3 2 BernPoly X 2 = 2 BernPoly X 3 2
108 35 85 86 divcli 3 2
109 mulcom 2 BernPoly X 3 2 2 BernPoly X 3 2 = 3 2 2 BernPoly X
110 103 108 109 sylancl X 2 BernPoly X 3 2 = 3 2 2 BernPoly X
111 bpoly2 X 2 BernPoly X = X 2 - X + 1 6
112 111 oveq2d X 3 2 2 BernPoly X = 3 2 X 2 - X + 1 6
113 sqcl X X 2
114 6cn 6
115 6re 6
116 6pos 0 < 6
117 115 116 gt0ne0ii 6 0
118 114 117 reccli 1 6
119 subsub X 2 X 1 6 X 2 X 1 6 = X 2 - X + 1 6
120 118 119 mp3an3 X 2 X X 2 X 1 6 = X 2 - X + 1 6
121 113 120 mpancom X X 2 X 1 6 = X 2 - X + 1 6
122 121 oveq2d X 3 2 X 2 X 1 6 = 3 2 X 2 - X + 1 6
123 subcl X 1 6 X 1 6
124 118 123 mpan2 X X 1 6
125 subdi 3 2 X 2 X 1 6 3 2 X 2 X 1 6 = 3 2 X 2 3 2 X 1 6
126 108 113 124 125 mp3an2i X 3 2 X 2 X 1 6 = 3 2 X 2 3 2 X 1 6
127 112 122 126 3eqtr2d X 3 2 2 BernPoly X = 3 2 X 2 3 2 X 1 6
128 107 110 127 3eqtrd X 3 2 BernPoly X 2 = 3 2 X 2 3 2 X 1 6
129 100 128 sylan9eqr X k = 2 ( 3 k) k BernPoly X 3 - k + 1 = 3 2 X 2 3 2 X 1 6
130 mulcl 3 2 X 2 3 2 X 2
131 108 113 130 sylancr X 3 2 X 2
132 mulcl 3 2 X 1 6 3 2 X 1 6
133 108 124 132 sylancr X 3 2 X 1 6
134 131 133 subcld X 3 2 X 2 3 2 X 1 6
135 134 adantr X k = 2 3 2 X 2 3 2 X 1 6
136 129 135 eqeltrd X k = 2 ( 3 k) k BernPoly X 3 - k + 1
137 52 79 136 3jaodan X k = 0 k = 1 k = 2 ( 3 k) k BernPoly X 3 - k + 1
138 27 137 sylan2b X k 0 1 + 1 ( 3 k) k BernPoly X 3 - k + 1
139 5 eqeq2i k = 2 k = 1 + 1
140 139 100 sylbir k = 1 + 1 ( 3 k) k BernPoly X 3 - k + 1 = 3 2 BernPoly X 2
141 10 138 140 fsump1 X k = 0 1 + 1 ( 3 k) k BernPoly X 3 - k + 1 = k = 0 1 ( 3 k) k BernPoly X 3 - k + 1 + 3 2 BernPoly X 2
142 128 oveq2d X k = 0 1 ( 3 k) k BernPoly X 3 - k + 1 + 3 2 BernPoly X 2 = k = 0 1 ( 3 k) k BernPoly X 3 - k + 1 + 3 2 X 2 - 3 2 X 1 6
143 15 sumeq1i k = 0 0 + 1 ( 3 k) k BernPoly X 3 - k + 1 = k = 0 1 ( 3 k) k BernPoly X 3 - k + 1
144 0nn0 0 0
145 nn0uz 0 = 0
146 144 145 eleqtri 0 0
147 146 a1i X 0 0
148 13 16 eqtri 0 0 + 1 = 0 1
149 148 eleq2i k 0 0 + 1 k 0 1
150 25 elpr k 0 1 k = 0 k = 1
151 149 150 bitri k 0 0 + 1 k = 0 k = 1
152 52 79 jaodan X k = 0 k = 1 ( 3 k) k BernPoly X 3 - k + 1
153 151 152 sylan2b X k 0 0 + 1 ( 3 k) k BernPoly X 3 - k + 1
154 14 eqeq2i k = 0 + 1 k = 1
155 154 65 sylbi k = 0 + 1 ( 3 k) k BernPoly X 3 - k + 1 = 3 1 BernPoly X 3
156 147 153 155 fsump1 X k = 0 0 + 1 ( 3 k) k BernPoly X 3 - k + 1 = k = 0 0 ( 3 k) k BernPoly X 3 - k + 1 + 3 1 BernPoly X 3
157 50 48 eqeltrdi X 1 0 BernPoly X 4
158 42 fsum1 0 1 0 BernPoly X 4 k = 0 0 ( 3 k) k BernPoly X 3 - k + 1 = 1 0 BernPoly X 4
159 11 157 158 sylancr X k = 0 0 ( 3 k) k BernPoly X 3 - k + 1 = 1 0 BernPoly X 4
160 159 50 eqtrd X k = 0 0 ( 3 k) k BernPoly X 3 - k + 1 = 1 4
161 160 76 oveq12d X k = 0 0 ( 3 k) k BernPoly X 3 - k + 1 + 3 1 BernPoly X 3 = 1 4 + X - 1 2
162 156 161 eqtrd X k = 0 0 + 1 ( 3 k) k BernPoly X 3 - k + 1 = 1 4 + X - 1 2
163 143 162 eqtr3id X k = 0 1 ( 3 k) k BernPoly X 3 - k + 1 = 1 4 + X - 1 2
164 163 oveq1d X k = 0 1 ( 3 k) k BernPoly X 3 - k + 1 + 3 2 X 2 - 3 2 X 1 6 = 1 4 + X 1 2 + 3 2 X 2 3 2 X 1 6
165 addcl 1 4 X 1 2 1 4 + X - 1 2
166 48 71 165 sylancr X 1 4 + X - 1 2
167 166 131 133 addsub12d X 1 4 + X 1 2 + 3 2 X 2 3 2 X 1 6 = 3 2 X 2 + 1 4 + X - 1 2 - 3 2 X 1 6
168 164 167 eqtrd X k = 0 1 ( 3 k) k BernPoly X 3 - k + 1 + 3 2 X 2 - 3 2 X 1 6 = 3 2 X 2 + 1 4 + X - 1 2 - 3 2 X 1 6
169 133 166 negsubdi2d X 3 2 X 1 6 1 4 + X - 1 2 = 1 4 + X 1 2 - 3 2 X 1 6
170 subdi 3 2 X 1 6 3 2 X 1 6 = 3 2 X 3 2 1 6
171 108 118 170 mp3an13 X 3 2 X 1 6 = 3 2 X 3 2 1 6
172 addsub12 1 4 X 1 2 1 4 + X - 1 2 = X + 1 4 - 1 2
173 48 69 172 mp3an13 X 1 4 + X - 1 2 = X + 1 4 - 1 2
174 171 173 oveq12d X 3 2 X 1 6 1 4 + X - 1 2 = 3 2 X - 3 2 1 6 - X + 1 4 - 1 2
175 mulcl 3 2 X 3 2 X
176 108 175 mpan X 3 2 X
177 108 118 mulcli 3 2 1 6
178 negsub 3 2 X 3 2 1 6 3 2 X + 3 2 1 6 = 3 2 X 3 2 1 6
179 176 177 178 sylancl X 3 2 X + 3 2 1 6 = 3 2 X 3 2 1 6
180 179 oveq1d X 3 2 X + 3 2 1 6 - X + 1 4 - 1 2 = 3 2 X - 3 2 1 6 - X + 1 4 - 1 2
181 69 48 negsubdi2i 1 2 1 4 = 1 4 1 2
182 85 35 85 mul12i 2 3 2 = 3 2 2
183 3t2e6 3 2 = 6
184 183 oveq2i 2 3 2 = 2 6
185 2t2e4 2 2 = 4
186 185 oveq2i 3 2 2 = 3 4
187 182 184 186 3eqtr3i 2 6 = 3 4
188 187 oveq2i 3 1 2 6 = 3 1 3 4
189 46 47 pm3.2i 4 4 0
190 35 72 pm3.2i 3 3 0
191 divcan5 1 4 4 0 3 3 0 3 1 3 4 = 1 4
192 60 189 190 191 mp3an 3 1 3 4 = 1 4
193 188 192 eqtri 3 1 2 6 = 1 4
194 35 85 60 114 86 117 divmuldivi 3 2 1 6 = 3 1 2 6
195 2t1e2 2 1 = 2
196 195 5 eqtri 2 1 = 1 + 1
197 196 185 oveq12i 2 1 2 2 = 1 + 1 4
198 divcan5 1 2 2 0 2 2 0 2 1 2 2 = 1 2
199 60 104 104 198 mp3an 2 1 2 2 = 1 2
200 60 60 46 47 divdiri 1 + 1 4 = 1 4 + 1 4
201 197 199 200 3eqtr3ri 1 4 + 1 4 = 1 2
202 69 48 48 201 subaddrii 1 2 1 4 = 1 4
203 193 194 202 3eqtr4ri 1 2 1 4 = 3 2 1 6
204 203 negeqi 1 2 1 4 = 3 2 1 6
205 181 204 eqtr3i 1 4 1 2 = 3 2 1 6
206 48 69 subcli 1 4 1 2
207 177 negcli 3 2 1 6
208 206 207 subeq0i 1 4 - 1 2 - 3 2 1 6 = 0 1 4 1 2 = 3 2 1 6
209 205 208 mpbir 1 4 - 1 2 - 3 2 1 6 = 0
210 209 oveq2i 3 2 X - X - 1 4 - 1 2 - 3 2 1 6 = 3 2 X - X - 0
211 id X X
212 206 a1i X 1 4 1 2
213 207 a1i X 3 2 1 6
214 176 211 212 213 subadd4d X 3 2 X - X - 1 4 - 1 2 - 3 2 1 6 = 3 2 X + 3 2 1 6 - X + 1 4 - 1 2
215 subdir 3 2 1 X 3 2 1 X = 3 2 X 1 X
216 108 60 215 mp3an12 X 3 2 1 X = 3 2 X 1 X
217 divsubdir 3 2 2 2 0 3 2 2 = 3 2 2 2
218 35 85 104 217 mp3an 3 2 2 = 3 2 2 2
219 95 oveq1i 3 2 2 = 1 2
220 2div2e1 2 2 = 1
221 220 oveq2i 3 2 2 2 = 3 2 1
222 218 219 221 3eqtr3ri 3 2 1 = 1 2
223 222 oveq1i 3 2 1 X = 1 2 X
224 223 a1i X 3 2 1 X = 1 2 X
225 mulid2 X 1 X = X
226 225 oveq2d X 3 2 X 1 X = 3 2 X X
227 216 224 226 3eqtr3rd X 3 2 X X = 1 2 X
228 227 oveq1d X 3 2 X - X - 0 = 1 2 X 0
229 mulcl 1 2 X 1 2 X
230 69 229 mpan X 1 2 X
231 230 subid1d X 1 2 X 0 = 1 2 X
232 228 231 eqtrd X 3 2 X - X - 0 = 1 2 X
233 210 214 232 3eqtr3a X 3 2 X + 3 2 1 6 - X + 1 4 - 1 2 = 1 2 X
234 174 180 233 3eqtr2d X 3 2 X 1 6 1 4 + X - 1 2 = 1 2 X
235 234 negeqd X 3 2 X 1 6 1 4 + X - 1 2 = 1 2 X
236 169 235 eqtr3d X 1 4 + X 1 2 - 3 2 X 1 6 = 1 2 X
237 236 oveq2d X 3 2 X 2 + 1 4 + X - 1 2 - 3 2 X 1 6 = 3 2 X 2 + 1 2 X
238 131 230 negsubd X 3 2 X 2 + 1 2 X = 3 2 X 2 1 2 X
239 168 237 238 3eqtrd X k = 0 1 ( 3 k) k BernPoly X 3 - k + 1 + 3 2 X 2 - 3 2 X 1 6 = 3 2 X 2 1 2 X
240 141 142 239 3eqtrd X k = 0 1 + 1 ( 3 k) k BernPoly X 3 - k + 1 = 3 2 X 2 1 2 X
241 8 240 eqtrid X k = 0 3 1 ( 3 k) k BernPoly X 3 - k + 1 = 3 2 X 2 1 2 X
242 241 oveq2d X X 3 k = 0 3 1 ( 3 k) k BernPoly X 3 - k + 1 = X 3 3 2 X 2 1 2 X
243 expcl X 3 0 X 3
244 1 243 mpan2 X X 3
245 244 131 230 subsubd X X 3 3 2 X 2 1 2 X = X 3 - 3 2 X 2 + 1 2 X
246 3 242 245 3eqtrd X 3 BernPoly X = X 3 - 3 2 X 2 + 1 2 X