Metamath Proof Explorer


Theorem bpoly2

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

Ref Expression
Assertion bpoly2 X 2 BernPoly X = X 2 - X + 1 6

Proof

Step Hyp Ref Expression
1 2nn0 2 0
2 bpolyval 2 0 X 2 BernPoly X = X 2 k = 0 2 1 ( 2 k) k BernPoly X 2 - k + 1
3 1 2 mpan X 2 BernPoly X = X 2 k = 0 2 1 ( 2 k) k BernPoly X 2 - k + 1
4 2m1e1 2 1 = 1
5 0p1e1 0 + 1 = 1
6 4 5 eqtr4i 2 1 = 0 + 1
7 6 oveq2i 0 2 1 = 0 0 + 1
8 7 sumeq1i k = 0 2 1 ( 2 k) k BernPoly X 2 - k + 1 = k = 0 0 + 1 ( 2 k) k BernPoly X 2 - k + 1
9 0nn0 0 0
10 nn0uz 0 = 0
11 9 10 eleqtri 0 0
12 11 a1i X 0 0
13 0z 0
14 fzpr 0 0 0 + 1 = 0 0 + 1
15 13 14 ax-mp 0 0 + 1 = 0 0 + 1
16 15 eleq2i k 0 0 + 1 k 0 0 + 1
17 vex k V
18 17 elpr k 0 0 + 1 k = 0 k = 0 + 1
19 16 18 bitri k 0 0 + 1 k = 0 k = 0 + 1
20 oveq2 k = 0 ( 2 k) = ( 2 0 )
21 bcn0 2 0 ( 2 0 ) = 1
22 1 21 ax-mp ( 2 0 ) = 1
23 20 22 eqtrdi k = 0 ( 2 k) = 1
24 oveq1 k = 0 k BernPoly X = 0 BernPoly X
25 oveq2 k = 0 2 k = 2 0
26 25 oveq1d k = 0 2 - k + 1 = 2 - 0 + 1
27 2cn 2
28 27 subid1i 2 0 = 2
29 28 oveq1i 2 - 0 + 1 = 2 + 1
30 df-3 3 = 2 + 1
31 29 30 eqtr4i 2 - 0 + 1 = 3
32 26 31 eqtrdi k = 0 2 - k + 1 = 3
33 24 32 oveq12d k = 0 k BernPoly X 2 - k + 1 = 0 BernPoly X 3
34 23 33 oveq12d k = 0 ( 2 k) k BernPoly X 2 - k + 1 = 1 0 BernPoly X 3
35 bpoly0 X 0 BernPoly X = 1
36 35 oveq1d X 0 BernPoly X 3 = 1 3
37 36 oveq2d X 1 0 BernPoly X 3 = 1 1 3
38 3cn 3
39 3ne0 3 0
40 38 39 reccli 1 3
41 40 mulid2i 1 1 3 = 1 3
42 37 41 eqtrdi X 1 0 BernPoly X 3 = 1 3
43 34 42 sylan9eqr X k = 0 ( 2 k) k BernPoly X 2 - k + 1 = 1 3
44 43 40 eqeltrdi X k = 0 ( 2 k) k BernPoly X 2 - k + 1
45 5 eqeq2i k = 0 + 1 k = 1
46 oveq2 k = 1 ( 2 k) = ( 2 1 )
47 bcn1 2 0 ( 2 1 ) = 2
48 1 47 ax-mp ( 2 1 ) = 2
49 46 48 eqtrdi k = 1 ( 2 k) = 2
50 oveq1 k = 1 k BernPoly X = 1 BernPoly X
51 oveq2 k = 1 2 k = 2 1
52 51 oveq1d k = 1 2 - k + 1 = 2 - 1 + 1
53 ax-1cn 1
54 npcan 2 1 2 - 1 + 1 = 2
55 27 53 54 mp2an 2 - 1 + 1 = 2
56 52 55 eqtrdi k = 1 2 - k + 1 = 2
57 50 56 oveq12d k = 1 k BernPoly X 2 - k + 1 = 1 BernPoly X 2
58 49 57 oveq12d k = 1 ( 2 k) k BernPoly X 2 - k + 1 = 2 1 BernPoly X 2
59 45 58 sylbi k = 0 + 1 ( 2 k) k BernPoly X 2 - k + 1 = 2 1 BernPoly X 2
60 bpoly1 X 1 BernPoly X = X 1 2
61 60 oveq1d X 1 BernPoly X 2 = X 1 2 2
62 61 oveq2d X 2 1 BernPoly X 2 = 2 X 1 2 2
63 halfcn 1 2
64 subcl X 1 2 X 1 2
65 63 64 mpan2 X X 1 2
66 2ne0 2 0
67 divcan2 X 1 2 2 2 0 2 X 1 2 2 = X 1 2
68 27 66 67 mp3an23 X 1 2 2 X 1 2 2 = X 1 2
69 65 68 syl X 2 X 1 2 2 = X 1 2
70 62 69 eqtrd X 2 1 BernPoly X 2 = X 1 2
71 59 70 sylan9eqr X k = 0 + 1 ( 2 k) k BernPoly X 2 - k + 1 = X 1 2
72 65 adantr X k = 0 + 1 X 1 2
73 71 72 eqeltrd X k = 0 + 1 ( 2 k) k BernPoly X 2 - k + 1
74 44 73 jaodan X k = 0 k = 0 + 1 ( 2 k) k BernPoly X 2 - k + 1
75 19 74 sylan2b X k 0 0 + 1 ( 2 k) k BernPoly X 2 - k + 1
76 12 75 59 fsump1 X k = 0 0 + 1 ( 2 k) k BernPoly X 2 - k + 1 = k = 0 0 ( 2 k) k BernPoly X 2 - k + 1 + 2 1 BernPoly X 2
77 42 40 eqeltrdi X 1 0 BernPoly X 3
78 34 fsum1 0 1 0 BernPoly X 3 k = 0 0 ( 2 k) k BernPoly X 2 - k + 1 = 1 0 BernPoly X 3
79 13 77 78 sylancr X k = 0 0 ( 2 k) k BernPoly X 2 - k + 1 = 1 0 BernPoly X 3
80 79 42 eqtrd X k = 0 0 ( 2 k) k BernPoly X 2 - k + 1 = 1 3
81 80 70 oveq12d X k = 0 0 ( 2 k) k BernPoly X 2 - k + 1 + 2 1 BernPoly X 2 = 1 3 + X - 1 2
82 76 81 eqtrd X k = 0 0 + 1 ( 2 k) k BernPoly X 2 - k + 1 = 1 3 + X - 1 2
83 addsub12 1 3 X 1 2 1 3 + X - 1 2 = X + 1 3 - 1 2
84 40 63 83 mp3an13 X 1 3 + X - 1 2 = X + 1 3 - 1 2
85 63 40 negsubdi2i 1 2 1 3 = 1 3 1 2
86 halfthird 1 2 1 3 = 1 6
87 86 negeqi 1 2 1 3 = 1 6
88 85 87 eqtr3i 1 3 1 2 = 1 6
89 88 oveq2i X + 1 3 - 1 2 = X + 1 6
90 84 89 eqtrdi X 1 3 + X - 1 2 = X + 1 6
91 6cn 6
92 6re 6
93 6pos 0 < 6
94 92 93 gt0ne0ii 6 0
95 91 94 reccli 1 6
96 negsub X 1 6 X + 1 6 = X 1 6
97 95 96 mpan2 X X + 1 6 = X 1 6
98 82 90 97 3eqtrd X k = 0 0 + 1 ( 2 k) k BernPoly X 2 - k + 1 = X 1 6
99 8 98 eqtrid X k = 0 2 1 ( 2 k) k BernPoly X 2 - k + 1 = X 1 6
100 99 oveq2d X X 2 k = 0 2 1 ( 2 k) k BernPoly X 2 - k + 1 = X 2 X 1 6
101 sqcl X X 2
102 subsub X 2 X 1 6 X 2 X 1 6 = X 2 - X + 1 6
103 95 102 mp3an3 X 2 X X 2 X 1 6 = X 2 - X + 1 6
104 101 103 mpancom X X 2 X 1 6 = X 2 - X + 1 6
105 3 100 104 3eqtrd X 2 BernPoly X = X 2 - X + 1 6