Definition df-bpoly 15991

Description: Define the Bernoulli polynomials. Here we use well-founded recursion to define the Bernoulli polynomials. This agrees with most textbook definitions, although explicit formulas 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 15990	. 2 class BernPoly
2		vm	. . 3 setvar 𝑚
3		vx	. . 3 setvar 𝑥
4		cn0 12472	. . 3 class ℕ0
5		cc 11108	. . 3 class ℂ
6	2	cv 1541	. . . 4 class 𝑚
7		clt 11248	. . . . 5 class <
8		vg	. . . . . 6 setvar 𝑔
9		cvv 3475	. . . . . 6 class V
10		vn	. . . . . . 7 setvar 𝑛
11	8	cv 1541	. . . . . . . . 9 class 𝑔
12	11	cdm 5677	. . . . . . . 8 class dom 𝑔
13		chash 14290	. . . . . . . 8 class ♯
14	12, 13	cfv 6544	. . . . . . 7 class (♯‘dom 𝑔)
15	3	cv 1541	. . . . . . . . 9 class 𝑥
16	10	cv 1541	. . . . . . . . 9 class 𝑛
17		cexp 14027	. . . . . . . . 9 class ↑
18	15, 16, 17	co 7409	. . . . . . . 8 class (𝑥↑𝑛)
19		vk	. . . . . . . . . . . 12 setvar 𝑘
20	19	cv 1541	. . . . . . . . . . 11 class 𝑘
21		cbc 14262	. . . . . . . . . . 11 class C
22	16, 20, 21	co 7409	. . . . . . . . . 10 class (𝑛C𝑘)
23	20, 11	cfv 6544	. . . . . . . . . . 11 class (𝑔‘𝑘)
24		cmin 11444	. . . . . . . . . . . . 13 class −
25	16, 20, 24	co 7409	. . . . . . . . . . . 12 class (𝑛 − 𝑘)
26		c1 11111	. . . . . . . . . . . 12 class 1
27		caddc 11113	. . . . . . . . . . . 12 class +
28	25, 26, 27	co 7409	. . . . . . . . . . 11 class ((𝑛 − 𝑘) + 1)
29		cdiv 11871	. . . . . . . . . . 11 class /
30	23, 28, 29	co 7409	. . . . . . . . . 10 class ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))
31		cmul 11115	. . . . . . . . . 10 class ·
32	22, 30, 31	co 7409	. . . . . . . . 9 class ((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))
33	12, 32, 19	csu 15632	. . . . . . . 8 class Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))
34	18, 33, 24	co 7409	. . . . . . 7 class ((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))
35	10, 14, 34	csb 3894	. . . . . 6 class ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))
36	8, 9, 35	cmpt 5232	. . . . 5 class (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))))
37	4, 7, 36	cwrecs 8296	. . . 4 class wrecs( < , ℕ0, (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))
38	6, 37	cfv 6544	. . 3 class (wrecs( < , ℕ0, (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚)
39	2, 3, 4, 5, 38	cmpo 7411	. 2 class (𝑚 ∈ ℕ0, 𝑥 ∈ ℂ ↦ (wrecs( < , ℕ0, (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚))
40	1, 39	wceq 1542	1 wff BernPoly = (𝑚 ∈ ℕ0, 𝑥 ∈ ℂ ↦ (wrecs( < , ℕ0, (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚))

This definition is referenced by:  bpolylem  15992