Metamath Proof Explorer

Theorem bpoly1

Description: The value of the Bernoulli polynomials at one. (Contributed by Scott Fenton, 16-May-2014)

Ref Expression
Assertion bpoly1 
|- ( X e. CC -> ( 1 BernPoly X ) = ( X - ( 1 / 2 ) ) )

Proof

Step Hyp Ref Expression
1 1nn0 
 |-  1 e. NN0
2 bpolyval 
 |-  ( ( 1 e. NN0 /\ X e. CC ) -> ( 1 BernPoly X ) = ( ( X ^ 1 ) - sum_ k e. ( 0 ... ( 1 - 1 ) ) ( ( 1 _C k ) x. ( ( k BernPoly X ) / ( ( 1 - k ) + 1 ) ) ) ) )
3 1 2 mpan 
 |-  ( X e. CC -> ( 1 BernPoly X ) = ( ( X ^ 1 ) - sum_ k e. ( 0 ... ( 1 - 1 ) ) ( ( 1 _C k ) x. ( ( k BernPoly X ) / ( ( 1 - k ) + 1 ) ) ) ) )
4 exp1 
 |-  ( X e. CC -> ( X ^ 1 ) = X )
5 1m1e0 
 |-  ( 1 - 1 ) = 0
6 5 oveq2i 
 |-  ( 0 ... ( 1 - 1 ) ) = ( 0 ... 0 )
7 6 sumeq1i 
 |-  sum_ k e. ( 0 ... ( 1 - 1 ) ) ( ( 1 _C k ) x. ( ( k BernPoly X ) / ( ( 1 - k ) + 1 ) ) ) = sum_ k e. ( 0 ... 0 ) ( ( 1 _C k ) x. ( ( k BernPoly X ) / ( ( 1 - k ) + 1 ) ) )
8 0z 
 |-  0 e. ZZ
9 bpoly0 
 |-  ( X e. CC -> ( 0 BernPoly X ) = 1 )
10 9 oveq1d 
 |-  ( X e. CC -> ( ( 0 BernPoly X ) / 2 ) = ( 1 / 2 ) )
11 10 oveq2d 
 |-  ( X e. CC -> ( 1 x. ( ( 0 BernPoly X ) / 2 ) ) = ( 1 x. ( 1 / 2 ) ) )
12 halfcn 
 |-  ( 1 / 2 ) e. CC
13 12 mulid2i 
 |-  ( 1 x. ( 1 / 2 ) ) = ( 1 / 2 )
14 11 13 eqtrdi 
 |-  ( X e. CC -> ( 1 x. ( ( 0 BernPoly X ) / 2 ) ) = ( 1 / 2 ) )
15 14 12 eqeltrdi 
 |-  ( X e. CC -> ( 1 x. ( ( 0 BernPoly X ) / 2 ) ) e. CC )
16 oveq2 
 |-  ( k = 0 -> ( 1 _C k ) = ( 1 _C 0 ) )
17 bcn0 
 |-  ( 1 e. NN0 -> ( 1 _C 0 ) = 1 )
18 1 17 ax-mp 
 |-  ( 1 _C 0 ) = 1
19 16 18 eqtrdi 
 |-  ( k = 0 -> ( 1 _C k ) = 1 )
20 oveq1 
 |-  ( k = 0 -> ( k BernPoly X ) = ( 0 BernPoly X ) )
21 oveq2 
 |-  ( k = 0 -> ( 1 - k ) = ( 1 - 0 ) )
22 1m0e1 
 |-  ( 1 - 0 ) = 1
23 21 22 eqtrdi 
 |-  ( k = 0 -> ( 1 - k ) = 1 )
24 23 oveq1d 
 |-  ( k = 0 -> ( ( 1 - k ) + 1 ) = ( 1 + 1 ) )
25 df-2 
 |-  2 = ( 1 + 1 )
26 24 25 eqtr4di 
 |-  ( k = 0 -> ( ( 1 - k ) + 1 ) = 2 )
27 20 26 oveq12d 
 |-  ( k = 0 -> ( ( k BernPoly X ) / ( ( 1 - k ) + 1 ) ) = ( ( 0 BernPoly X ) / 2 ) )
28 19 27 oveq12d 
 |-  ( k = 0 -> ( ( 1 _C k ) x. ( ( k BernPoly X ) / ( ( 1 - k ) + 1 ) ) ) = ( 1 x. ( ( 0 BernPoly X ) / 2 ) ) )
29 28 fsum1 
 |-  ( ( 0 e. ZZ /\ ( 1 x. ( ( 0 BernPoly X ) / 2 ) ) e. CC ) -> sum_ k e. ( 0 ... 0 ) ( ( 1 _C k ) x. ( ( k BernPoly X ) / ( ( 1 - k ) + 1 ) ) ) = ( 1 x. ( ( 0 BernPoly X ) / 2 ) ) )
30 8 15 29 sylancr 
 |-  ( X e. CC -> sum_ k e. ( 0 ... 0 ) ( ( 1 _C k ) x. ( ( k BernPoly X ) / ( ( 1 - k ) + 1 ) ) ) = ( 1 x. ( ( 0 BernPoly X ) / 2 ) ) )
31 30 14 eqtrd 
 |-  ( X e. CC -> sum_ k e. ( 0 ... 0 ) ( ( 1 _C k ) x. ( ( k BernPoly X ) / ( ( 1 - k ) + 1 ) ) ) = ( 1 / 2 ) )
32 7 31 eqtrid 
 |-  ( X e. CC -> sum_ k e. ( 0 ... ( 1 - 1 ) ) ( ( 1 _C k ) x. ( ( k BernPoly X ) / ( ( 1 - k ) + 1 ) ) ) = ( 1 / 2 ) )
33 4 32 oveq12d 
 |-  ( X e. CC -> ( ( X ^ 1 ) - sum_ k e. ( 0 ... ( 1 - 1 ) ) ( ( 1 _C k ) x. ( ( k BernPoly X ) / ( ( 1 - k ) + 1 ) ) ) ) = ( X - ( 1 / 2 ) ) )
34 3 33 eqtrd 
 |-  ( X e. CC -> ( 1 BernPoly X ) = ( X - ( 1 / 2 ) ) )