Definition df-bpoly 14617

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 = (𝑚 ∈ ℕ0, 𝑥 ∈ ℂ ↦ (wrecs( < , ℕ0, (𝑔 ∈ V ↦ ⦋(#‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚))

Distinct variable group:   𝑔,𝑘,𝑚,𝑛,𝑥

Detailed syntax breakdown of Definition df-bpoly

Step	Hyp	Ref	Expression
1		cbp 14616	. 2 class BernPoly
2		vm	. . 3 setvar 𝑚
3		vx	. . 3 setvar 𝑥
4		cn0 11169	. . 3 class ℕ0
5		cc 9813	. . 3 class ℂ
6	2	cv 1474	. . . 4 class 𝑚
7		clt 9953	. . . . 5 class <
8		vg	. . . . . 6 setvar 𝑔
9		cvv 3173	. . . . . 6 class V
10		vn	. . . . . . 7 setvar 𝑛
11	8	cv 1474	. . . . . . . . 9 class 𝑔
12	11	cdm 5038	. . . . . . . 8 class dom 𝑔
13		chash 12979	. . . . . . . 8 class #
14	12, 13	cfv 5804	. . . . . . 7 class (#‘dom 𝑔)
15	3	cv 1474	. . . . . . . . 9 class 𝑥
16	10	cv 1474	. . . . . . . . 9 class 𝑛
17		cexp 12722	. . . . . . . . 9 class ↑
18	15, 16, 17	co 6549	. . . . . . . 8 class (𝑥↑𝑛)
19		vk	. . . . . . . . . . . 12 setvar 𝑘
20	19	cv 1474	. . . . . . . . . . 11 class 𝑘
21		cbc 12951	. . . . . . . . . . 11 class C
22	16, 20, 21	co 6549	. . . . . . . . . 10 class (𝑛C𝑘)
23	20, 11	cfv 5804	. . . . . . . . . . 11 class (𝑔‘𝑘)
24		cmin 10145	. . . . . . . . . . . . 13 class −
25	16, 20, 24	co 6549	. . . . . . . . . . . 12 class (𝑛 − 𝑘)
26		c1 9816	. . . . . . . . . . . 12 class 1
27		caddc 9818	. . . . . . . . . . . 12 class +
28	25, 26, 27	co 6549	. . . . . . . . . . 11 class ((𝑛 − 𝑘) + 1)
29		cdiv 10563	. . . . . . . . . . 11 class /
30	23, 28, 29	co 6549	. . . . . . . . . 10 class ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))
31		cmul 9820	. . . . . . . . . 10 class ·
32	22, 30, 31	co 6549	. . . . . . . . 9 class ((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))
33	12, 32, 19	csu 14264	. . . . . . . 8 class Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))
34	18, 33, 24	co 6549	. . . . . . 7 class ((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))
35	10, 14, 34	csb 3499	. . . . . 6 class ⦋(#‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))
36	8, 9, 35	cmpt 4643	. . . . 5 class (𝑔 ∈ V ↦ ⦋(#‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))))
37	4, 7, 36	cwrecs 7293	. . . 4 class wrecs( < , ℕ0, (𝑔 ∈ V ↦ ⦋(#‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))
38	6, 37	cfv 5804	. . 3 class (wrecs( < , ℕ0, (𝑔 ∈ V ↦ ⦋(#‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚)
39	2, 3, 4, 5, 38	cmpt2 6551	. 2 class (𝑚 ∈ ℕ0, 𝑥 ∈ ℂ ↦ (wrecs( < , ℕ0, (𝑔 ∈ V ↦ ⦋(#‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚))
40	1, 39	wceq 1475	1 wff BernPoly = (𝑚 ∈ ℕ0, 𝑥 ∈ ℂ ↦ (wrecs( < , ℕ0, (𝑔 ∈ V ↦ ⦋(#‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚))

This definition is referenced by:  bpolylem  14618