Definition df-bpoly 14778

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

Step	Hyp	Ref	Expression
1		cbp 14777	. 2 class BernPoly
2		vm	. . 3 setvar m
3		vx	. . 3 setvar x
4		cn0 11292	. . 3 class NN0
5		cc 9934	. . 3 class CC
6	2	cv 1482	. . . 4 class m
7		clt 10074	. . . . 5 class <
8		vg	. . . . . 6 setvar g
9		cvv 3200	. . . . . 6 class _V
10		vn	. . . . . . 7 setvar n
11	8	cv 1482	. . . . . . . . 9 class g
12	11	cdm 5114	. . . . . . . 8 class dom g
13		chash 13117	. . . . . . . 8 class #
14	12, 13	cfv 5888	. . . . . . 7 class ( # ` dom g )
15	3	cv 1482	. . . . . . . . 9 class x
16	10	cv 1482	. . . . . . . . 9 class n
17		cexp 12860	. . . . . . . . 9 class ^
18	15, 16, 17	co 6650	. . . . . . . 8 class ( x ^ n )
19		vk	. . . . . . . . . . . 12 setvar k
20	19	cv 1482	. . . . . . . . . . 11 class k
21		cbc 13089	. . . . . . . . . . 11 class _C
22	16, 20, 21	co 6650	. . . . . . . . . 10 class ( n _C k )
23	20, 11	cfv 5888	. . . . . . . . . . 11 class ( g ` k )
24		cmin 10266	. . . . . . . . . . . . 13 class -
25	16, 20, 24	co 6650	. . . . . . . . . . . 12 class ( n - k )
26		c1 9937	. . . . . . . . . . . 12 class 1
27		caddc 9939	. . . . . . . . . . . 12 class +
28	25, 26, 27	co 6650	. . . . . . . . . . 11 class ( ( n - k ) + 1 )
29		cdiv 10684	. . . . . . . . . . 11 class /
30	23, 28, 29	co 6650	. . . . . . . . . 10 class ( ( g ` k ) / ( ( n - k ) + 1 ) )
31		cmul 9941	. . . . . . . . . 10 class x.
32	22, 30, 31	co 6650	. . . . . . . . 9 class ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) )
33	12, 32, 19	csu 14416	. . . . . . . 8 class sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) )
34	18, 33, 24	co 6650	. . . . . . 7 class ( ( x ^ n ) - sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) )
35	10, 14, 34	csb 3533	. . . . . 6 class [_ ( # ` dom g ) / n ]_ ( ( x ^ n ) - sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) )
36	8, 9, 35	cmpt 4729	. . . . 5 class ( g e. _V |-> [_ ( # ` dom g ) / n ]_ ( ( x ^ n ) - sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) ) )
37	4, 7, 36	cwrecs 7406	. . . 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 ) ) ) ) ) )
38	6, 37	cfv 5888	. . 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 )
39	2, 3, 4, 5, 38	cmpt2 6652	. 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 ) )
40	1, 39	wceq 1483	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 ) )

This definition is referenced by:  bpolylem  14779