Metamath Proof Explorer

Definition df-bpoly

Description: Define the Bernoulli polynomials. Here we use well-founded recursion to define the Bernoulli polynomials. This agrees with most textbook definitions, although explicit formulas do exist. (Contributed by Scott Fenton, 22-May-2014)

Ref Expression
Assertion df-bpoly 
|- BernPoly = ( m e. NN0 , x e. CC |-> ( wrecs ( < , NN0 , ( g e. _V |-> [_ ( # ` dom g ) / n ]_ ( ( x ^ n ) - sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) ) ) ) ` m ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cbp 
 |-  BernPoly
1 vm 
 |-  m
2 cn0 
 |-  NN0
3 vx 
 |-  x
4 cc 
 |-  CC
5 clt 
 |-  <
6 vg 
 |-  g
7 cvv 
 |-  _V
8 chash 
 |-  #
9 6 cv 
 |-  g
10 9 cdm 
 |-  dom g
11 10 8 cfv 
 |-  ( # ` dom g )
12 vn 
 |-  n
13 3 cv 
 |-  x
14 cexp 
 |-  ^
15 12 cv 
 |-  n
16 13 15 14 co 
 |-  ( x ^ n )
17 cmin 
 |-  -
18 vk 
 |-  k
19 cbc 
 |-  _C
20 18 cv 
 |-  k
21 15 20 19 co 
 |-  ( n _C k )
22 cmul 
 |-  x.
23 20 9 cfv 
 |-  ( g ` k )
24 cdiv 
 |-  /
25 15 20 17 co 
 |-  ( n - k )
26 caddc 
 |-  +
27 c1 
 |-  1
28 25 27 26 co 
 |-  ( ( n - k ) + 1 )
29 23 28 24 co 
 |-  ( ( g ` k ) / ( ( n - k ) + 1 ) )
30 21 29 22 co 
 |-  ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) )
31 10 30 18 csu 
 |-  sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) )
32 16 31 17 co 
 |-  ( ( x ^ n ) - sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) )
33 12 11 32 csb 
 |-  [_ ( # ` dom g ) / n ]_ ( ( x ^ n ) - sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) )
34 6 7 33 cmpt 
 |-  ( g e. _V |-> [_ ( # ` dom g ) / n ]_ ( ( x ^ n ) - sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) ) )
35 2 5 34 cwrecs 
 |-  wrecs ( < , NN0 , ( g e. _V |-> [_ ( # ` dom g ) / n ]_ ( ( x ^ n ) - sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) ) ) )
36 1 cv 
 |-  m
37 36 35 cfv 
 |-  ( wrecs ( < , NN0 , ( g e. _V |-> [_ ( # ` dom g ) / n ]_ ( ( x ^ n ) - sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) ) ) ) ` m )
38 1 3 2 4 37 cmpo 
 |-  ( m e. NN0 , x e. CC |-> ( wrecs ( < , NN0 , ( g e. _V |-> [_ ( # ` dom g ) / n ]_ ( ( x ^ n ) - sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) ) ) ) ` m ) )
39 0 38 wceq 
 |-  BernPoly = ( m e. NN0 , x e. CC |-> ( wrecs ( < , NN0 , ( g e. _V |-> [_ ( # ` dom g ) / n ]_ ( ( x ^ n ) - sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) ) ) ) ` m ) )