Metamath Proof Explorer

Theorem bpoly2

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

Ref Expression
Assertion bpoly2 
|- ( X e. CC -> ( 2 BernPoly X ) = ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) )

Proof

Step Hyp Ref Expression
1 2nn0 
 |-  2 e. NN0
2 bpolyval 
 |-  ( ( 2 e. NN0 /\ X e. CC ) -> ( 2 BernPoly X ) = ( ( X ^ 2 ) - sum_ k e. ( 0 ... ( 2 - 1 ) ) ( ( 2 _C k ) x. ( ( k BernPoly X ) / ( ( 2 - k ) + 1 ) ) ) ) )
3 1 2 mpan 
 |-  ( X e. CC -> ( 2 BernPoly X ) = ( ( X ^ 2 ) - sum_ k e. ( 0 ... ( 2 - 1 ) ) ( ( 2 _C k ) x. ( ( 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 
 |-  sum_ k e. ( 0 ... ( 2 - 1 ) ) ( ( 2 _C k ) x. ( ( k BernPoly X ) / ( ( 2 - k ) + 1 ) ) ) = sum_ k e. ( 0 ... ( 0 + 1 ) ) ( ( 2 _C k ) x. ( ( k BernPoly X ) / ( ( 2 - k ) + 1 ) ) )
9 0nn0 
 |-  0 e. NN0
10 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
11 9 10 eleqtri 
 |-  0 e. ( ZZ>= ` 0 )
12 11 a1i 
 |-  ( X e. CC -> 0 e. ( ZZ>= ` 0 ) )
13 0z 
 |-  0 e. ZZ
14 fzpr 
 |-  ( 0 e. ZZ -> ( 0 ... ( 0 + 1 ) ) = { 0 , ( 0 + 1 ) } )
15 13 14 ax-mp 
 |-  ( 0 ... ( 0 + 1 ) ) = { 0 , ( 0 + 1 ) }
16 15 eleq2i 
 |-  ( k e. ( 0 ... ( 0 + 1 ) ) <-> k e. { 0 , ( 0 + 1 ) } )
17 vex 
 |-  k e. _V
18 17 elpr 
 |-  ( k e. { 0 , ( 0 + 1 ) } <-> ( k = 0 \/ k = ( 0 + 1 ) ) )
19 16 18 bitri 
 |-  ( k e. ( 0 ... ( 0 + 1 ) ) <-> ( k = 0 \/ k = ( 0 + 1 ) ) )
20 oveq2 
 |-  ( k = 0 -> ( 2 _C k ) = ( 2 _C 0 ) )
21 bcn0 
 |-  ( 2 e. NN0 -> ( 2 _C 0 ) = 1 )
22 1 21 ax-mp 
 |-  ( 2 _C 0 ) = 1
23 20 22 eqtrdi 
 |-  ( k = 0 -> ( 2 _C 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 e. CC
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 _C k ) x. ( ( k BernPoly X ) / ( ( 2 - k ) + 1 ) ) ) = ( 1 x. ( ( 0 BernPoly X ) / 3 ) ) )
35 bpoly0 
 |-  ( X e. CC -> ( 0 BernPoly X ) = 1 )
36 35 oveq1d 
 |-  ( X e. CC -> ( ( 0 BernPoly X ) / 3 ) = ( 1 / 3 ) )
37 36 oveq2d 
 |-  ( X e. CC -> ( 1 x. ( ( 0 BernPoly X ) / 3 ) ) = ( 1 x. ( 1 / 3 ) ) )
38 3cn 
 |-  3 e. CC
39 3ne0 
 |-  3 =/= 0
40 38 39 reccli 
 |-  ( 1 / 3 ) e. CC
41 40 mulid2i 
 |-  ( 1 x. ( 1 / 3 ) ) = ( 1 / 3 )
42 37 41 eqtrdi 
 |-  ( X e. CC -> ( 1 x. ( ( 0 BernPoly X ) / 3 ) ) = ( 1 / 3 ) )
43 34 42 sylan9eqr 
 |-  ( ( X e. CC /\ k = 0 ) -> ( ( 2 _C k ) x. ( ( k BernPoly X ) / ( ( 2 - k ) + 1 ) ) ) = ( 1 / 3 ) )
44 43 40 eqeltrdi 
 |-  ( ( X e. CC /\ k = 0 ) -> ( ( 2 _C k ) x. ( ( k BernPoly X ) / ( ( 2 - k ) + 1 ) ) ) e. CC )
45 5 eqeq2i 
 |-  ( k = ( 0 + 1 ) <-> k = 1 )
46 oveq2 
 |-  ( k = 1 -> ( 2 _C k ) = ( 2 _C 1 ) )
47 bcn1 
 |-  ( 2 e. NN0 -> ( 2 _C 1 ) = 2 )
48 1 47 ax-mp 
 |-  ( 2 _C 1 ) = 2
49 46 48 eqtrdi 
 |-  ( k = 1 -> ( 2 _C 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 e. CC
54 npcan 
 |-  ( ( 2 e. CC /\ 1 e. CC ) -> ( ( 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 _C k ) x. ( ( k BernPoly X ) / ( ( 2 - k ) + 1 ) ) ) = ( 2 x. ( ( 1 BernPoly X ) / 2 ) ) )
59 45 58 sylbi 
 |-  ( k = ( 0 + 1 ) -> ( ( 2 _C k ) x. ( ( k BernPoly X ) / ( ( 2 - k ) + 1 ) ) ) = ( 2 x. ( ( 1 BernPoly X ) / 2 ) ) )
60 bpoly1 
 |-  ( X e. CC -> ( 1 BernPoly X ) = ( X - ( 1 / 2 ) ) )
61 60 oveq1d 
 |-  ( X e. CC -> ( ( 1 BernPoly X ) / 2 ) = ( ( X - ( 1 / 2 ) ) / 2 ) )
62 61 oveq2d 
 |-  ( X e. CC -> ( 2 x. ( ( 1 BernPoly X ) / 2 ) ) = ( 2 x. ( ( X - ( 1 / 2 ) ) / 2 ) ) )
63 halfcn 
 |-  ( 1 / 2 ) e. CC
64 subcl 
 |-  ( ( X e. CC /\ ( 1 / 2 ) e. CC ) -> ( X - ( 1 / 2 ) ) e. CC )
65 63 64 mpan2 
 |-  ( X e. CC -> ( X - ( 1 / 2 ) ) e. CC )
66 2ne0 
 |-  2 =/= 0
67 divcan2 
 |-  ( ( ( X - ( 1 / 2 ) ) e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( 2 x. ( ( X - ( 1 / 2 ) ) / 2 ) ) = ( X - ( 1 / 2 ) ) )
68 27 66 67 mp3an23 
 |-  ( ( X - ( 1 / 2 ) ) e. CC -> ( 2 x. ( ( X - ( 1 / 2 ) ) / 2 ) ) = ( X - ( 1 / 2 ) ) )
69 65 68 syl 
 |-  ( X e. CC -> ( 2 x. ( ( X - ( 1 / 2 ) ) / 2 ) ) = ( X - ( 1 / 2 ) ) )
70 62 69 eqtrd 
 |-  ( X e. CC -> ( 2 x. ( ( 1 BernPoly X ) / 2 ) ) = ( X - ( 1 / 2 ) ) )
71 59 70 sylan9eqr 
 |-  ( ( X e. CC /\ k = ( 0 + 1 ) ) -> ( ( 2 _C k ) x. ( ( k BernPoly X ) / ( ( 2 - k ) + 1 ) ) ) = ( X - ( 1 / 2 ) ) )
72 65 adantr 
 |-  ( ( X e. CC /\ k = ( 0 + 1 ) ) -> ( X - ( 1 / 2 ) ) e. CC )
73 71 72 eqeltrd 
 |-  ( ( X e. CC /\ k = ( 0 + 1 ) ) -> ( ( 2 _C k ) x. ( ( k BernPoly X ) / ( ( 2 - k ) + 1 ) ) ) e. CC )
74 44 73 jaodan 
 |-  ( ( X e. CC /\ ( k = 0 \/ k = ( 0 + 1 ) ) ) -> ( ( 2 _C k ) x. ( ( k BernPoly X ) / ( ( 2 - k ) + 1 ) ) ) e. CC )
75 19 74 sylan2b 
 |-  ( ( X e. CC /\ k e. ( 0 ... ( 0 + 1 ) ) ) -> ( ( 2 _C k ) x. ( ( k BernPoly X ) / ( ( 2 - k ) + 1 ) ) ) e. CC )
76 12 75 59 fsump1 
 |-  ( X e. CC -> sum_ k e. ( 0 ... ( 0 + 1 ) ) ( ( 2 _C k ) x. ( ( k BernPoly X ) / ( ( 2 - k ) + 1 ) ) ) = ( sum_ k e. ( 0 ... 0 ) ( ( 2 _C k ) x. ( ( k BernPoly X ) / ( ( 2 - k ) + 1 ) ) ) + ( 2 x. ( ( 1 BernPoly X ) / 2 ) ) ) )
77 42 40 eqeltrdi 
 |-  ( X e. CC -> ( 1 x. ( ( 0 BernPoly X ) / 3 ) ) e. CC )
78 34 fsum1 
 |-  ( ( 0 e. ZZ /\ ( 1 x. ( ( 0 BernPoly X ) / 3 ) ) e. CC ) -> sum_ k e. ( 0 ... 0 ) ( ( 2 _C k ) x. ( ( k BernPoly X ) / ( ( 2 - k ) + 1 ) ) ) = ( 1 x. ( ( 0 BernPoly X ) / 3 ) ) )
79 13 77 78 sylancr 
 |-  ( X e. CC -> sum_ k e. ( 0 ... 0 ) ( ( 2 _C k ) x. ( ( k BernPoly X ) / ( ( 2 - k ) + 1 ) ) ) = ( 1 x. ( ( 0 BernPoly X ) / 3 ) ) )
80 79 42 eqtrd 
 |-  ( X e. CC -> sum_ k e. ( 0 ... 0 ) ( ( 2 _C k ) x. ( ( k BernPoly X ) / ( ( 2 - k ) + 1 ) ) ) = ( 1 / 3 ) )
81 80 70 oveq12d 
 |-  ( X e. CC -> ( sum_ k e. ( 0 ... 0 ) ( ( 2 _C k ) x. ( ( k BernPoly X ) / ( ( 2 - k ) + 1 ) ) ) + ( 2 x. ( ( 1 BernPoly X ) / 2 ) ) ) = ( ( 1 / 3 ) + ( X - ( 1 / 2 ) ) ) )
82 76 81 eqtrd 
 |-  ( X e. CC -> sum_ k e. ( 0 ... ( 0 + 1 ) ) ( ( 2 _C k ) x. ( ( k BernPoly X ) / ( ( 2 - k ) + 1 ) ) ) = ( ( 1 / 3 ) + ( X - ( 1 / 2 ) ) ) )
83 addsub12 
 |-  ( ( ( 1 / 3 ) e. CC /\ X e. CC /\ ( 1 / 2 ) e. CC ) -> ( ( 1 / 3 ) + ( X - ( 1 / 2 ) ) ) = ( X + ( ( 1 / 3 ) - ( 1 / 2 ) ) ) )
84 40 63 83 mp3an13 
 |-  ( X e. CC -> ( ( 1 / 3 ) + ( X - ( 1 / 2 ) ) ) = ( X + ( ( 1 / 3 ) - ( 1 / 2 ) ) ) )
85 63 40 negsubdi2i 
 |-  -u ( ( 1 / 2 ) - ( 1 / 3 ) ) = ( ( 1 / 3 ) - ( 1 / 2 ) )
86 halfthird 
 |-  ( ( 1 / 2 ) - ( 1 / 3 ) ) = ( 1 / 6 )
87 86 negeqi 
 |-  -u ( ( 1 / 2 ) - ( 1 / 3 ) ) = -u ( 1 / 6 )
88 85 87 eqtr3i 
 |-  ( ( 1 / 3 ) - ( 1 / 2 ) ) = -u ( 1 / 6 )
89 88 oveq2i 
 |-  ( X + ( ( 1 / 3 ) - ( 1 / 2 ) ) ) = ( X + -u ( 1 / 6 ) )
90 84 89 eqtrdi 
 |-  ( X e. CC -> ( ( 1 / 3 ) + ( X - ( 1 / 2 ) ) ) = ( X + -u ( 1 / 6 ) ) )
91 6cn 
 |-  6 e. CC
92 6re 
 |-  6 e. RR
93 6pos 
 |-  0 < 6
94 92 93 gt0ne0ii 
 |-  6 =/= 0
95 91 94 reccli 
 |-  ( 1 / 6 ) e. CC
96 negsub 
 |-  ( ( X e. CC /\ ( 1 / 6 ) e. CC ) -> ( X + -u ( 1 / 6 ) ) = ( X - ( 1 / 6 ) ) )
97 95 96 mpan2 
 |-  ( X e. CC -> ( X + -u ( 1 / 6 ) ) = ( X - ( 1 / 6 ) ) )
98 82 90 97 3eqtrd 
 |-  ( X e. CC -> sum_ k e. ( 0 ... ( 0 + 1 ) ) ( ( 2 _C k ) x. ( ( k BernPoly X ) / ( ( 2 - k ) + 1 ) ) ) = ( X - ( 1 / 6 ) ) )
99 8 98 eqtrid 
 |-  ( X e. CC -> sum_ k e. ( 0 ... ( 2 - 1 ) ) ( ( 2 _C k ) x. ( ( k BernPoly X ) / ( ( 2 - k ) + 1 ) ) ) = ( X - ( 1 / 6 ) ) )
100 99 oveq2d 
 |-  ( X e. CC -> ( ( X ^ 2 ) - sum_ k e. ( 0 ... ( 2 - 1 ) ) ( ( 2 _C k ) x. ( ( k BernPoly X ) / ( ( 2 - k ) + 1 ) ) ) ) = ( ( X ^ 2 ) - ( X - ( 1 / 6 ) ) ) )
101 sqcl 
 |-  ( X e. CC -> ( X ^ 2 ) e. CC )
102 subsub 
 |-  ( ( ( X ^ 2 ) e. CC /\ X e. CC /\ ( 1 / 6 ) e. CC ) -> ( ( X ^ 2 ) - ( X - ( 1 / 6 ) ) ) = ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) )
103 95 102 mp3an3 
 |-  ( ( ( X ^ 2 ) e. CC /\ X e. CC ) -> ( ( X ^ 2 ) - ( X - ( 1 / 6 ) ) ) = ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) )
104 101 103 mpancom 
 |-  ( X e. CC -> ( ( X ^ 2 ) - ( X - ( 1 / 6 ) ) ) = ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) )
105 3 100 104 3eqtrd 
 |-  ( X e. CC -> ( 2 BernPoly X ) = ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) )