Definition df-bpoly 16137

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 16136	. 2 class BernPoly
2		vm	. . 3 setvar 𝑚
3		vx	. . 3 setvar 𝑥
4		cn0 12531	. . 3 class ℕ0
5		cc 11125	. . 3 class ℂ
6	2	cv 1569	. . . 4 class 𝑚
7		clt 11270	. . . . 5 class <
8		vg	. . . . . 6 setvar 𝑔
9		cvv 3453	. . . . . 6 class V
10		vn	. . . . . . 7 setvar 𝑛
11	8	cv 1569	. . . . . . . . 9 class 𝑔
12	11	cdm 5659	. . . . . . . 8 class dom 𝑔
13		chash 14396	. . . . . . . 8 class ♯
14	12, 13	cfv 6537	. . . . . . 7 class (♯‘dom 𝑔)
15	3	cv 1569	. . . . . . . . 9 class 𝑥
16	10	cv 1569	. . . . . . . . 9 class 𝑛
17		cexp 14127	. . . . . . . . 9 class ↑
18	15, 16, 17	co 7416	. . . . . . . 8 class (𝑥↑𝑛)
19		vk	. . . . . . . . . . . 12 setvar 𝑘
20	19	cv 1569	. . . . . . . . . . 11 class 𝑘
21		cbc 14368	. . . . . . . . . . 11 class C
22	16, 20, 21	co 7416	. . . . . . . . . 10 class (𝑛C𝑘)
23	20, 11	cfv 6537	. . . . . . . . . . 11 class (𝑔‘𝑘)
24		cmin 11468	. . . . . . . . . . . . 13 class −
25	16, 20, 24	co 7416	. . . . . . . . . . . 12 class (𝑛 − 𝑘)
26		c1 11128	. . . . . . . . . . . 12 class 1
27		caddc 11130	. . . . . . . . . . . 12 class +
28	25, 26, 27	co 7416	. . . . . . . . . . 11 class ((𝑛 − 𝑘) + 1)
29		cdiv 11898	. . . . . . . . . . 11 class /
30	23, 28, 29	co 7416	. . . . . . . . . 10 class ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))
31		cmul 11132	. . . . . . . . . 10 class ·
32	22, 30, 31	co 7416	. . . . . . . . 9 class ((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))
33	12, 32, 19	csu 15775	. . . . . . . 8 class Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))
34	18, 33, 24	co 7416	. . . . . . 7 class ((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))
35	10, 14, 34	csb 3850	. . . . . 6 class ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))
36	8, 9, 35	cmpt 5190	. . . . 5 class (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))))
37	4, 7, 36	cwrecs 8313	. . . 4 class wrecs( < , ℕ0, (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))
38	6, 37	cfv 6537	. . 3 class (wrecs( < , ℕ0, (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚)
39	2, 3, 4, 5, 38	cmpo 7418	. 2 class (𝑚 ∈ ℕ0, 𝑥 ∈ ℂ ↦ (wrecs( < , ℕ0, (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚))
40	1, 39	wceq 1570	1 wff BernPoly = (𝑚 ∈ ℕ0, 𝑥 ∈ ℂ ↦ (wrecs( < , ℕ0, (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚))

This definition is used by:  bpolylem  16138