Metamath Proof Explorer

Theorem bpolyval

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

Ref Expression
Assertion bpolyval 
|- ( ( N e. NN0 /\ X e. CC ) -> ( N BernPoly X ) = ( ( X ^ N ) - sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fvex 
 |-  ( # ` dom c ) e. _V
2 oveq2 
 |-  ( n = ( # ` dom c ) -> ( X ^ n ) = ( X ^ ( # ` dom c ) ) )
3 oveq1 
 |-  ( n = ( # ` dom c ) -> ( n _C m ) = ( ( # ` dom c ) _C m ) )
4 oveq1 
 |-  ( n = ( # ` dom c ) -> ( n - m ) = ( ( # ` dom c ) - m ) )
5 4 oveq1d 
 |-  ( n = ( # ` dom c ) -> ( ( n - m ) + 1 ) = ( ( ( # ` dom c ) - m ) + 1 ) )
6 5 oveq2d 
 |-  ( n = ( # ` dom c ) -> ( ( c ` m ) / ( ( n - m ) + 1 ) ) = ( ( c ` m ) / ( ( ( # ` dom c ) - m ) + 1 ) ) )
7 3 6 oveq12d 
 |-  ( n = ( # ` dom c ) -> ( ( n _C m ) x. ( ( c ` m ) / ( ( n - m ) + 1 ) ) ) = ( ( ( # ` dom c ) _C m ) x. ( ( c ` m ) / ( ( ( # ` dom c ) - m ) + 1 ) ) ) )
8 7 sumeq2sdv 
 |-  ( n = ( # ` dom c ) -> sum_ m e. dom c ( ( n _C m ) x. ( ( c ` m ) / ( ( n - m ) + 1 ) ) ) = sum_ m e. dom c ( ( ( # ` dom c ) _C m ) x. ( ( c ` m ) / ( ( ( # ` dom c ) - m ) + 1 ) ) ) )
9 2 8 oveq12d 
 |-  ( n = ( # ` dom c ) -> ( ( X ^ n ) - sum_ m e. dom c ( ( n _C m ) x. ( ( c ` m ) / ( ( n - m ) + 1 ) ) ) ) = ( ( X ^ ( # ` dom c ) ) - sum_ m e. dom c ( ( ( # ` dom c ) _C m ) x. ( ( c ` m ) / ( ( ( # ` dom c ) - m ) + 1 ) ) ) ) )
10 1 9 csbie 
 |-  [_ ( # ` dom c ) / n ]_ ( ( X ^ n ) - sum_ m e. dom c ( ( n _C m ) x. ( ( c ` m ) / ( ( n - m ) + 1 ) ) ) ) = ( ( X ^ ( # ` dom c ) ) - sum_ m e. dom c ( ( ( # ` dom c ) _C m ) x. ( ( c ` m ) / ( ( ( # ` dom c ) - m ) + 1 ) ) ) )
11 oveq2 
 |-  ( m = k -> ( n _C m ) = ( n _C k ) )
12 fveq2 
 |-  ( m = k -> ( c ` m ) = ( c ` k ) )
13 oveq2 
 |-  ( m = k -> ( n - m ) = ( n - k ) )
14 13 oveq1d 
 |-  ( m = k -> ( ( n - m ) + 1 ) = ( ( n - k ) + 1 ) )
15 12 14 oveq12d 
 |-  ( m = k -> ( ( c ` m ) / ( ( n - m ) + 1 ) ) = ( ( c ` k ) / ( ( n - k ) + 1 ) ) )
16 11 15 oveq12d 
 |-  ( m = k -> ( ( n _C m ) x. ( ( c ` m ) / ( ( n - m ) + 1 ) ) ) = ( ( n _C k ) x. ( ( c ` k ) / ( ( n - k ) + 1 ) ) ) )
17 16 cbvsumv 
 |-  sum_ m e. dom c ( ( n _C m ) x. ( ( c ` m ) / ( ( n - m ) + 1 ) ) ) = sum_ k e. dom c ( ( n _C k ) x. ( ( c ` k ) / ( ( n - k ) + 1 ) ) )
18 dmeq 
 |-  ( c = g -> dom c = dom g )
19 fveq1 
 |-  ( c = g -> ( c ` k ) = ( g ` k ) )
20 19 oveq1d 
 |-  ( c = g -> ( ( c ` k ) / ( ( n - k ) + 1 ) ) = ( ( g ` k ) / ( ( n - k ) + 1 ) ) )
21 20 oveq2d 
 |-  ( c = g -> ( ( n _C k ) x. ( ( c ` k ) / ( ( n - k ) + 1 ) ) ) = ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) )
22 21 adantr 
 |-  ( ( c = g /\ k e. dom c ) -> ( ( n _C k ) x. ( ( c ` k ) / ( ( n - k ) + 1 ) ) ) = ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) )
23 18 22 sumeq12dv 
 |-  ( c = g -> sum_ k e. dom c ( ( n _C k ) x. ( ( c ` k ) / ( ( n - k ) + 1 ) ) ) = sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) )
24 17 23 eqtrid 
 |-  ( c = g -> sum_ m e. dom c ( ( n _C m ) x. ( ( c ` m ) / ( ( n - m ) + 1 ) ) ) = sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) )
25 24 oveq2d 
 |-  ( c = g -> ( ( X ^ n ) - sum_ m e. dom c ( ( n _C m ) x. ( ( c ` m ) / ( ( n - m ) + 1 ) ) ) ) = ( ( X ^ n ) - sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) ) )
26 25 csbeq2dv 
 |-  ( c = g -> [_ ( # ` dom c ) / n ]_ ( ( X ^ n ) - sum_ m e. dom c ( ( n _C m ) x. ( ( c ` m ) / ( ( n - m ) + 1 ) ) ) ) = [_ ( # ` dom c ) / n ]_ ( ( X ^ n ) - sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) ) )
27 10 26 eqtr3id 
 |-  ( c = g -> ( ( X ^ ( # ` dom c ) ) - sum_ m e. dom c ( ( ( # ` dom c ) _C m ) x. ( ( c ` m ) / ( ( ( # ` dom c ) - m ) + 1 ) ) ) ) = [_ ( # ` dom c ) / n ]_ ( ( X ^ n ) - sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) ) )
28 18 fveq2d 
 |-  ( c = g -> ( # ` dom c ) = ( # ` dom g ) )
29 28 csbeq1d 
 |-  ( c = g -> [_ ( # ` dom c ) / n ]_ ( ( X ^ n ) - sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) ) = [_ ( # ` dom g ) / n ]_ ( ( X ^ n ) - sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) ) )
30 27 29 eqtrd 
 |-  ( c = g -> ( ( X ^ ( # ` dom c ) ) - sum_ m e. dom c ( ( ( # ` dom c ) _C m ) x. ( ( c ` m ) / ( ( ( # ` dom c ) - m ) + 1 ) ) ) ) = [_ ( # ` dom g ) / n ]_ ( ( X ^ n ) - sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) ) )
31 30 cbvmptv 
 |-  ( c e. _V |-> ( ( X ^ ( # ` dom c ) ) - sum_ m e. dom c ( ( ( # ` dom c ) _C m ) x. ( ( c ` m ) / ( ( ( # ` dom c ) - m ) + 1 ) ) ) ) ) = ( g e. _V |-> [_ ( # ` dom g ) / n ]_ ( ( X ^ n ) - sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) ) )
32 eqid 
 |-  wrecs ( < , NN0 , ( c e. _V |-> ( ( X ^ ( # ` dom c ) ) - sum_ m e. dom c ( ( ( # ` dom c ) _C m ) x. ( ( c ` m ) / ( ( ( # ` dom c ) - m ) + 1 ) ) ) ) ) ) = wrecs ( < , NN0 , ( c e. _V |-> ( ( X ^ ( # ` dom c ) ) - sum_ m e. dom c ( ( ( # ` dom c ) _C m ) x. ( ( c ` m ) / ( ( ( # ` dom c ) - m ) + 1 ) ) ) ) ) )
33 31 32 bpolylem 
 |-  ( ( N e. NN0 /\ X e. CC ) -> ( N BernPoly X ) = ( ( X ^ N ) - sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) ) )