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 28141
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 28140 . 2  class BernPoly
2 vm . . 3  setvar  m
3 vx . . 3  setvar  x
4 cn0 10571 . . 3  class  NN0
5 cc 9272 . . 3  class  CC
62cv 1368 . . . 4  class  m
7 clt 9410 . . . . 5  class  <
8 vg . . . . . 6  setvar  g
9 cvv 2967 . . . . . 6  class  _V
10 vn . . . . . . 7  setvar  n
118cv 1368 . . . . . . . . 9  class  g
1211cdm 4835 . . . . . . . 8  class  dom  g
13 chash 12095 . . . . . . . 8  class  #
1412, 13cfv 5413 . . . . . . 7  class  ( # `  dom  g )
153cv 1368 . . . . . . . . 9  class  x
1610cv 1368 . . . . . . . . 9  class  n
17 cexp 11857 . . . . . . . . 9  class  ^
1815, 16, 17co 6086 . . . . . . . 8  class  ( x ^ n )
19 vk . . . . . . . . . . . 12  setvar  k
2019cv 1368 . . . . . . . . . . 11  class  k
21 cbc 12070 . . . . . . . . . . 11  class  _C
2216, 20, 21co 6086 . . . . . . . . . 10  class  ( n  _C  k )
2320, 11cfv 5413 . . . . . . . . . . 11  class  ( g `
 k )
24 cmin 9587 . . . . . . . . . . . . 13  class  -
2516, 20, 24co 6086 . . . . . . . . . . . 12  class  ( n  -  k )
26 c1 9275 . . . . . . . . . . . 12  class  1
27 caddc 9277 . . . . . . . . . . . 12  class  +
2825, 26, 27co 6086 . . . . . . . . . . 11  class  ( ( n  -  k )  +  1 )
29 cdiv 9985 . . . . . . . . . . 11  class  /
3023, 28, 29co 6086 . . . . . . . . . 10  class  ( ( g `  k )  /  ( ( n  -  k )  +  1 ) )
31 cmul 9279 . . . . . . . . . 10  class  x.
3222, 30, 31co 6086 . . . . . . . . 9  class  ( ( n  _C  k )  x.  ( ( g `
 k )  / 
( ( n  -  k )  +  1 ) ) )
3312, 32, 19csu 13155 . . . . . . . 8  class  sum_ k  e.  dom  g ( ( n  _C  k )  x.  ( ( g `
 k )  / 
( ( n  -  k )  +  1 ) ) )
3418, 33, 24co 6086 . . . . . . 7  class  ( ( x ^ n )  -  sum_ k  e.  dom  g ( ( n  _C  k )  x.  ( ( g `  k )  /  (
( n  -  k
)  +  1 ) ) ) )
3510, 14, 34csb 3283 . . . . . 6  class  [_ ( # `
 dom  g )  /  n ]_ ( ( x ^ n )  -  sum_ k  e.  dom  g ( ( n  _C  k )  x.  ( ( g `  k )  /  (
( n  -  k
)  +  1 ) ) ) )
368, 9, 35cmpt 4345 . . . . 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 27667 . . . 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 5413 . . 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 6088 . 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 1369 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 setvar class
This definition is referenced by:  bpolylem  28142
  Copyright terms: Public domain W3C validator