Metamath Proof Explorer

Theorem bpoly0

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

Ref Expression
Assertion bpoly0 
|- ( X e. CC -> ( 0 BernPoly X ) = 1 )

Proof

Step Hyp Ref Expression
1 0nn0 
 |-  0 e. NN0
2 bpolyval 
 |-  ( ( 0 e. NN0 /\ X e. CC ) -> ( 0 BernPoly X ) = ( ( X ^ 0 ) - sum_ k e. ( 0 ... ( 0 - 1 ) ) ( ( 0 _C k ) x. ( ( k BernPoly X ) / ( ( 0 - k ) + 1 ) ) ) ) )
3 1 2 mpan 
 |-  ( X e. CC -> ( 0 BernPoly X ) = ( ( X ^ 0 ) - sum_ k e. ( 0 ... ( 0 - 1 ) ) ( ( 0 _C k ) x. ( ( k BernPoly X ) / ( ( 0 - k ) + 1 ) ) ) ) )
4 exp0 
 |-  ( X e. CC -> ( X ^ 0 ) = 1 )
5 4 oveq1d 
 |-  ( X e. CC -> ( ( X ^ 0 ) - sum_ k e. ( 0 ... ( 0 - 1 ) ) ( ( 0 _C k ) x. ( ( k BernPoly X ) / ( ( 0 - k ) + 1 ) ) ) ) = ( 1 - sum_ k e. ( 0 ... ( 0 - 1 ) ) ( ( 0 _C k ) x. ( ( k BernPoly X ) / ( ( 0 - k ) + 1 ) ) ) ) )
6 risefall0lem 
 |-  ( 0 ... ( 0 - 1 ) ) = (/)
7 6 sumeq1i 
 |-  sum_ k e. ( 0 ... ( 0 - 1 ) ) ( ( 0 _C k ) x. ( ( k BernPoly X ) / ( ( 0 - k ) + 1 ) ) ) = sum_ k e. (/) ( ( 0 _C k ) x. ( ( k BernPoly X ) / ( ( 0 - k ) + 1 ) ) )
8 sum0 
 |-  sum_ k e. (/) ( ( 0 _C k ) x. ( ( k BernPoly X ) / ( ( 0 - k ) + 1 ) ) ) = 0
9 7 8 eqtri 
 |-  sum_ k e. ( 0 ... ( 0 - 1 ) ) ( ( 0 _C k ) x. ( ( k BernPoly X ) / ( ( 0 - k ) + 1 ) ) ) = 0
10 9 oveq2i 
 |-  ( 1 - sum_ k e. ( 0 ... ( 0 - 1 ) ) ( ( 0 _C k ) x. ( ( k BernPoly X ) / ( ( 0 - k ) + 1 ) ) ) ) = ( 1 - 0 )
11 1m0e1 
 |-  ( 1 - 0 ) = 1
12 10 11 eqtri 
 |-  ( 1 - sum_ k e. ( 0 ... ( 0 - 1 ) ) ( ( 0 _C k ) x. ( ( k BernPoly X ) / ( ( 0 - k ) + 1 ) ) ) ) = 1
13 5 12 eqtrdi 
 |-  ( X e. CC -> ( ( X ^ 0 ) - sum_ k e. ( 0 ... ( 0 - 1 ) ) ( ( 0 _C k ) x. ( ( k BernPoly X ) / ( ( 0 - k ) + 1 ) ) ) ) = 1 )
14 3 13 eqtrd 
 |-  ( X e. CC -> ( 0 BernPoly X ) = 1 )