Definition df-bpoly 15395

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 15394	. 2 class BernPoly
2		vm	. . 3 setvar 𝑚
3		vx	. . 3 setvar 𝑥
4		cn0 11891	. . 3 class ℕ0
5		cc 10529	. . 3 class ℂ
6	2	cv 1532	. . . 4 class 𝑚
7		clt 10669	. . . . 5 class <
8		vg	. . . . . 6 setvar 𝑔
9		cvv 3495	. . . . . 6 class V
10		vn	. . . . . . 7 setvar 𝑛
11	8	cv 1532	. . . . . . . . 9 class 𝑔
12	11	cdm 5550	. . . . . . . 8 class dom 𝑔
13		chash 13684	. . . . . . . 8 class ♯
14	12, 13	cfv 6350	. . . . . . 7 class (♯‘dom 𝑔)
15	3	cv 1532	. . . . . . . . 9 class 𝑥
16	10	cv 1532	. . . . . . . . 9 class 𝑛
17		cexp 13423	. . . . . . . . 9 class ↑
18	15, 16, 17	co 7150	. . . . . . . 8 class (𝑥↑𝑛)
19		vk	. . . . . . . . . . . 12 setvar 𝑘
20	19	cv 1532	. . . . . . . . . . 11 class 𝑘
21		cbc 13656	. . . . . . . . . . 11 class C
22	16, 20, 21	co 7150	. . . . . . . . . 10 class (𝑛C𝑘)
23	20, 11	cfv 6350	. . . . . . . . . . 11 class (𝑔‘𝑘)
24		cmin 10864	. . . . . . . . . . . . 13 class −
25	16, 20, 24	co 7150	. . . . . . . . . . . 12 class (𝑛 − 𝑘)
26		c1 10532	. . . . . . . . . . . 12 class 1
27		caddc 10534	. . . . . . . . . . . 12 class +
28	25, 26, 27	co 7150	. . . . . . . . . . 11 class ((𝑛 − 𝑘) + 1)
29		cdiv 11291	. . . . . . . . . . 11 class /
30	23, 28, 29	co 7150	. . . . . . . . . 10 class ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))
31		cmul 10536	. . . . . . . . . 10 class ·
32	22, 30, 31	co 7150	. . . . . . . . 9 class ((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))
33	12, 32, 19	csu 15036	. . . . . . . 8 class Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))
34	18, 33, 24	co 7150	. . . . . . 7 class ((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))
35	10, 14, 34	csb 3883	. . . . . 6 class ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))
36	8, 9, 35	cmpt 5139	. . . . 5 class (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))))
37	4, 7, 36	cwrecs 7940	. . . 4 class wrecs( < , ℕ0, (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))
38	6, 37	cfv 6350	. . 3 class (wrecs( < , ℕ0, (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚)
39	2, 3, 4, 5, 38	cmpo 7152	. 2 class (𝑚 ∈ ℕ0, 𝑥 ∈ ℂ ↦ (wrecs( < , ℕ0, (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚))
40	1, 39	wceq 1533	1 wff BernPoly = (𝑚 ∈ ℕ0, 𝑥 ∈ ℂ ↦ (wrecs( < , ℕ0, (𝑔 ∈ V ↦ ⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚))

This definition is referenced by:  bpolylem  15396