Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bpoly Structured version   Unicode version

Definition df-bpoly 26098
Description: Define the Bernoulli polynomials. Here we use well-founded recursion to define the Bernoulli polynomials. This agrees with most textbook definitions, although explicit formulae do exist. (Contributed by Scott Fenton, 22-May-2014.)
Assertion
Ref Expression
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 ) )
Distinct variable group:    g, k, m, n, x

Detailed syntax breakdown of Definition df-bpoly
StepHypRef Expression
1 cbp 26097 . 2  class BernPoly
2 vm . . 3  set  m
3 vx . . 3  set  x
4 cn0 10226 . . 3  class  NN0
5 cc 8993 . . 3  class  CC
62cv 1652 . . . 4  class  m
7 clt 9125 . . . . 5  class  <
8 vg . . . . . 6  set  g
9 cvv 2958 . . . . . 6  class  _V
10 vn . . . . . . 7  set  n
118cv 1652 . . . . . . . . 9  class  g
1211cdm 4881 . . . . . . . 8  class  dom  g
13 chash 11623 . . . . . . . 8  class  #
1412, 13cfv 5457 . . . . . . 7  class  ( # `  dom  g )
153cv 1652 . . . . . . . . 9  class  x
1610cv 1652 . . . . . . . . 9  class  n
17 cexp 11387 . . . . . . . . 9  class  ^
1815, 16, 17co 6084 . . . . . . . 8  class  ( x ^ n )
19 vk . . . . . . . . . . . 12  set  k
2019cv 1652 . . . . . . . . . . 11  class  k
21 cbc 11598 . . . . . . . . . . 11  class  _C
2216, 20, 21co 6084 . . . . . . . . . 10  class  ( n  _C  k )
2320, 11cfv 5457 . . . . . . . . . . 11  class  ( g `
 k )
24 cmin 9296 . . . . . . . . . . . . 13  class  -
2516, 20, 24co 6084 . . . . . . . . . . . 12  class  ( n  -  k )
26 c1 8996 . . . . . . . . . . . 12  class  1
27 caddc 8998 . . . . . . . . . . . 12  class  +
2825, 26, 27co 6084 . . . . . . . . . . 11  class  ( ( n  -  k )  +  1 )
29 cdiv 9682 . . . . . . . . . . 11  class  /
3023, 28, 29co 6084 . . . . . . . . . 10  class  ( ( g `  k )  /  ( ( n  -  k )  +  1 ) )
31 cmul 9000 . . . . . . . . . 10  class  x.
3222, 30, 31co 6084 . . . . . . . . 9  class  ( ( n  _C  k )  x.  ( ( g `
 k )  / 
( ( n  -  k )  +  1 ) ) )
3312, 32, 19csu 12484 . . . . . . . 8  class  sum_ k  e.  dom  g ( ( n  _C  k )  x.  ( ( g `
 k )  / 
( ( n  -  k )  +  1 ) ) )
3418, 33, 24co 6084 . . . . . . 7  class  ( ( x ^ n )  -  sum_ k  e.  dom  g ( ( n  _C  k )  x.  ( ( g `  k )  /  (
( n  -  k
)  +  1 ) ) ) )
3510, 14, 34csb 3253 . . . . . 6  class  [_ ( # `
 dom  g )  /  n ]_ ( ( x ^ n )  -  sum_ k  e.  dom  g ( ( n  _C  k )  x.  ( ( g `  k )  /  (
( n  -  k
)  +  1 ) ) ) )
368, 9, 35cmpt 4269 . . . . 5  class  ( g  e.  _V  |->  [_ ( # `
 dom  g )  /  n ]_ ( ( x ^ n )  -  sum_ k  e.  dom  g ( ( n  _C  k )  x.  ( ( g `  k )  /  (
( n  -  k
)  +  1 ) ) ) ) )
374, 7, 36cwrecs 25535 . . . 4  class wrecs (  <  ,  NN0 ,  ( g  e.  _V  |->  [_ ( # `
 dom  g )  /  n ]_ ( ( x ^ n )  -  sum_ k  e.  dom  g ( ( n  _C  k )  x.  ( ( g `  k )  /  (
( n  -  k
)  +  1 ) ) ) ) ) )
386, 37cfv 5457 . . 3  class  (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 )
392, 3, 4, 5, 38cmpt2 6086 . 2  class  ( 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 ) )
401, 39wceq 1653 1  wff 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 ) )
Colors of variables: wff set class
This definition is referenced by:  bpolylem  26099
  Copyright terms: Public domain W3C validator