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

Definition df-bpoly 24782
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  |->  ( U. { f  |  E. s ( f  Fn  s  /\  ( s 
C_  NN0  /\  A. e  e.  s  Pred (  <  ,  NN0 ,  e ) 
C_  s )  /\  A. e  e.  s  ( f `  e )  =  ( ( g  e.  _V  |->  [_ ( # `
 dom  g )  /  n ]_ ( ( x ^ n )  -  sum_ k  e.  dom  g ( ( n  _C  k )  x.  ( ( g `  k )  /  (
( n  -  k
)  +  1 ) ) ) ) ) `
 ( f  |`  Pred (  <  ,  NN0 ,  e ) ) ) ) } `  m
) )
Distinct variable group:    e, f, g, k, m, n, s, x

Detailed syntax breakdown of Definition df-bpoly
StepHypRef Expression
1 cbp 24781 . 2  class BernPoly
2 vm . . 3  set  m
3 vx . . 3  set  x
4 cn0 9965 . . 3  class  NN0
5 cc 8735 . . 3  class  CC
62cv 1622 . . . 4  class  m
7 vf . . . . . . . . . 10  set  f
87cv 1622 . . . . . . . . 9  class  f
9 vs . . . . . . . . . 10  set  s
109cv 1622 . . . . . . . . 9  class  s
118, 10wfn 5250 . . . . . . . 8  wff  f  Fn  s
1210, 4wss 3152 . . . . . . . . 9  wff  s  C_  NN0
13 clt 8867 . . . . . . . . . . . 12  class  <
14 ve . . . . . . . . . . . . 13  set  e
1514cv 1622 . . . . . . . . . . . 12  class  e
164, 13, 15cpred 24167 . . . . . . . . . . 11  class  Pred (  <  ,  NN0 ,  e )
1716, 10wss 3152 . . . . . . . . . 10  wff  Pred (  <  ,  NN0 ,  e )  C_  s
1817, 14, 10wral 2543 . . . . . . . . 9  wff  A. e  e.  s  Pred (  <  ,  NN0 ,  e ) 
C_  s
1912, 18wa 358 . . . . . . . 8  wff  ( s 
C_  NN0  /\  A. e  e.  s  Pred (  <  ,  NN0 ,  e ) 
C_  s )
2015, 8cfv 5255 . . . . . . . . . 10  class  ( f `
 e )
218, 16cres 4691 . . . . . . . . . . 11  class  ( f  |`  Pred (  <  ,  NN0 ,  e ) )
22 vg . . . . . . . . . . . 12  set  g
23 cvv 2788 . . . . . . . . . . . 12  class  _V
24 vn . . . . . . . . . . . . 13  set  n
2522cv 1622 . . . . . . . . . . . . . . 15  class  g
2625cdm 4689 . . . . . . . . . . . . . 14  class  dom  g
27 chash 11337 . . . . . . . . . . . . . 14  class  #
2826, 27cfv 5255 . . . . . . . . . . . . 13  class  ( # `  dom  g )
293cv 1622 . . . . . . . . . . . . . . 15  class  x
3024cv 1622 . . . . . . . . . . . . . . 15  class  n
31 cexp 11104 . . . . . . . . . . . . . . 15  class  ^
3229, 30, 31co 5858 . . . . . . . . . . . . . 14  class  ( x ^ n )
33 vk . . . . . . . . . . . . . . . . . 18  set  k
3433cv 1622 . . . . . . . . . . . . . . . . 17  class  k
35 cbc 11315 . . . . . . . . . . . . . . . . 17  class  _C
3630, 34, 35co 5858 . . . . . . . . . . . . . . . 16  class  ( n  _C  k )
3734, 25cfv 5255 . . . . . . . . . . . . . . . . 17  class  ( g `
 k )
38 cmin 9037 . . . . . . . . . . . . . . . . . . 19  class  -
3930, 34, 38co 5858 . . . . . . . . . . . . . . . . . 18  class  ( n  -  k )
40 c1 8738 . . . . . . . . . . . . . . . . . 18  class  1
41 caddc 8740 . . . . . . . . . . . . . . . . . 18  class  +
4239, 40, 41co 5858 . . . . . . . . . . . . . . . . 17  class  ( ( n  -  k )  +  1 )
43 cdiv 9423 . . . . . . . . . . . . . . . . 17  class  /
4437, 42, 43co 5858 . . . . . . . . . . . . . . . 16  class  ( ( g `  k )  /  ( ( n  -  k )  +  1 ) )
45 cmul 8742 . . . . . . . . . . . . . . . 16  class  x.
4636, 44, 45co 5858 . . . . . . . . . . . . . . 15  class  ( ( n  _C  k )  x.  ( ( g `
 k )  / 
( ( n  -  k )  +  1 ) ) )
4726, 46, 33csu 12158 . . . . . . . . . . . . . 14  class  sum_ k  e.  dom  g ( ( n  _C  k )  x.  ( ( g `
 k )  / 
( ( n  -  k )  +  1 ) ) )
4832, 47, 38co 5858 . . . . . . . . . . . . 13  class  ( ( x ^ n )  -  sum_ k  e.  dom  g ( ( n  _C  k )  x.  ( ( g `  k )  /  (
( n  -  k
)  +  1 ) ) ) )
4924, 28, 48csb 3081 . . . . . . . . . . . 12  class  [_ ( # `
 dom  g )  /  n ]_ ( ( x ^ n )  -  sum_ k  e.  dom  g ( ( n  _C  k )  x.  ( ( g `  k )  /  (
( n  -  k
)  +  1 ) ) ) )
5022, 23, 49cmpt 4077 . . . . . . . . . . 11  class  ( g  e.  _V  |->  [_ ( # `
 dom  g )  /  n ]_ ( ( x ^ n )  -  sum_ k  e.  dom  g ( ( n  _C  k )  x.  ( ( g `  k )  /  (
( n  -  k
)  +  1 ) ) ) ) )
5121, 50cfv 5255 . . . . . . . . . 10  class  ( ( g  e.  _V  |->  [_ ( # `  dom  g
)  /  n ]_ ( ( x ^
n )  -  sum_ k  e.  dom  g ( ( n  _C  k
)  x.  ( ( g `  k )  /  ( ( n  -  k )  +  1 ) ) ) ) ) `  (
f  |`  Pred (  <  ,  NN0 ,  e ) ) )
5220, 51wceq 1623 . . . . . . . . 9  wff  ( f `
 e )  =  ( ( g  e. 
_V  |->  [_ ( # `  dom  g )  /  n ]_ ( ( x ^
n )  -  sum_ k  e.  dom  g ( ( n  _C  k
)  x.  ( ( g `  k )  /  ( ( n  -  k )  +  1 ) ) ) ) ) `  (
f  |`  Pred (  <  ,  NN0 ,  e ) ) )
5352, 14, 10wral 2543 . . . . . . . 8  wff  A. e  e.  s  ( f `  e )  =  ( ( g  e.  _V  |->  [_ ( # `  dom  g )  /  n ]_ ( ( x ^
n )  -  sum_ k  e.  dom  g ( ( n  _C  k
)  x.  ( ( g `  k )  /  ( ( n  -  k )  +  1 ) ) ) ) ) `  (
f  |`  Pred (  <  ,  NN0 ,  e ) ) )
5411, 19, 53w3a 934 . . . . . . 7  wff  ( f  Fn  s  /\  (
s  C_  NN0  /\  A. e  e.  s  Pred (  <  ,  NN0 , 
e )  C_  s
)  /\  A. e  e.  s  ( f `  e )  =  ( ( g  e.  _V  |->  [_ ( # `  dom  g )  /  n ]_ ( ( x ^
n )  -  sum_ k  e.  dom  g ( ( n  _C  k
)  x.  ( ( g `  k )  /  ( ( n  -  k )  +  1 ) ) ) ) ) `  (
f  |`  Pred (  <  ,  NN0 ,  e ) ) ) )
5554, 9wex 1528 . . . . . 6  wff  E. s
( f  Fn  s  /\  ( s  C_  NN0  /\  A. e  e.  s  Pred (  <  ,  NN0 , 
e )  C_  s
)  /\  A. e  e.  s  ( f `  e )  =  ( ( g  e.  _V  |->  [_ ( # `  dom  g )  /  n ]_ ( ( x ^
n )  -  sum_ k  e.  dom  g ( ( n  _C  k
)  x.  ( ( g `  k )  /  ( ( n  -  k )  +  1 ) ) ) ) ) `  (
f  |`  Pred (  <  ,  NN0 ,  e ) ) ) )
5655, 7cab 2269 . . . . 5  class  { f  |  E. s ( f  Fn  s  /\  ( s  C_  NN0  /\  A. e  e.  s  Pred (  <  ,  NN0 , 
e )  C_  s
)  /\  A. e  e.  s  ( f `  e )  =  ( ( g  e.  _V  |->  [_ ( # `  dom  g )  /  n ]_ ( ( x ^
n )  -  sum_ k  e.  dom  g ( ( n  _C  k
)  x.  ( ( g `  k )  /  ( ( n  -  k )  +  1 ) ) ) ) ) `  (
f  |`  Pred (  <  ,  NN0 ,  e ) ) ) ) }
5756cuni 3827 . . . 4  class  U. {
f  |  E. s
( f  Fn  s  /\  ( s  C_  NN0  /\  A. e  e.  s  Pred (  <  ,  NN0 , 
e )  C_  s
)  /\  A. e  e.  s  ( f `  e )  =  ( ( g  e.  _V  |->  [_ ( # `  dom  g )  /  n ]_ ( ( x ^
n )  -  sum_ k  e.  dom  g ( ( n  _C  k
)  x.  ( ( g `  k )  /  ( ( n  -  k )  +  1 ) ) ) ) ) `  (
f  |`  Pred (  <  ,  NN0 ,  e ) ) ) ) }
586, 57cfv 5255 . . 3  class  ( U. { f  |  E. s ( f  Fn  s  /\  ( s 
C_  NN0  /\  A. e  e.  s  Pred (  <  ,  NN0 ,  e ) 
C_  s )  /\  A. e  e.  s  ( f `  e )  =  ( ( g  e.  _V  |->  [_ ( # `
 dom  g )  /  n ]_ ( ( x ^ n )  -  sum_ k  e.  dom  g ( ( n  _C  k )  x.  ( ( g `  k )  /  (
( n  -  k
)  +  1 ) ) ) ) ) `
 ( f  |`  Pred (  <  ,  NN0 ,  e ) ) ) ) } `  m
)
592, 3, 4, 5, 58cmpt2 5860 . 2  class  ( m  e.  NN0 ,  x  e.  CC  |->  ( U. {
f  |  E. s
( f  Fn  s  /\  ( s  C_  NN0  /\  A. e  e.  s  Pred (  <  ,  NN0 , 
e )  C_  s
)  /\  A. e  e.  s  ( f `  e )  =  ( ( g  e.  _V  |->  [_ ( # `  dom  g )  /  n ]_ ( ( x ^
n )  -  sum_ k  e.  dom  g ( ( n  _C  k
)  x.  ( ( g `  k )  /  ( ( n  -  k )  +  1 ) ) ) ) ) `  (
f  |`  Pred (  <  ,  NN0 ,  e ) ) ) ) } `  m ) )
601, 59wceq 1623 1  wff BernPoly  =  ( m  e.  NN0 ,  x  e.  CC  |->  ( U. { f  |  E. s ( f  Fn  s  /\  ( s 
C_  NN0  /\  A. e  e.  s  Pred (  <  ,  NN0 ,  e ) 
C_  s )  /\  A. e  e.  s  ( f `  e )  =  ( ( g  e.  _V  |->  [_ ( # `
 dom  g )  /  n ]_ ( ( x ^ n )  -  sum_ k  e.  dom  g ( ( n  _C  k )  x.  ( ( g `  k )  /  (
( n  -  k
)  +  1 ) ) ) ) ) `
 ( f  |`  Pred (  <  ,  NN0 ,  e ) ) ) ) } `  m
) )
Colors of variables: wff set class
This definition is referenced by:  bpolylem  24783
  Copyright terms: Public domain W3C validator