Metamath Proof Explorer

Definition df-bpoly

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)

Ref Expression
Assertion df-bpoly ⊢BernPoly=m∈ℕ0,x∈ℂ⟼wrecs⁡<ℕ0g∈V⟼⦋dom⁡g/n⦌xn−∑k∈dom⁡g(nk)⁢g⁡kn-k+1⁡m

Detailed syntax breakdown

Step Hyp Ref Expression
0 cbp classBernPoly
1 vm setvarm
2 cn0 classℕ0
3 vx setvarx
4 cc classℂ
5 clt class<
6 vg setvarg
7 cvv classV
8 chash class.
9 6 cv setvarg
10 9 cdm classdom⁡g
11 10 8 cfv classdom⁡g
12 vn setvarn
13 3 cv setvarx
14 cexp class^
15 12 cv setvarn
16 13 15 14 co classxn
17 cmin class−
18 vk setvark
19 cbc class(..)
20 18 cv setvark
21 15 20 19 co class(nk)
22 cmul class×
23 20 9 cfv classg⁡k
24 cdiv class÷
25 15 20 17 co classn−k
26 caddc class+
27 c1 class1
28 25 27 26 co classn-k+1
29 23 28 24 co classg⁡kn-k+1
30 21 29 22 co class(nk)⁢g⁡kn-k+1
31 10 30 18 csu class∑k∈dom⁡g(nk)⁢g⁡kn-k+1
32 16 31 17 co classxn−∑k∈dom⁡g(nk)⁢g⁡kn-k+1
33 12 11 32 csb class⦋dom⁡g/n⦌xn−∑k∈dom⁡g(nk)⁢g⁡kn-k+1
34 6 7 33 cmpt classg∈V⟼⦋dom⁡g/n⦌xn−∑k∈dom⁡g(nk)⁢g⁡kn-k+1
35 2 5 34 cwrecs classwrecs⁡<ℕ0g∈V⟼⦋dom⁡g/n⦌xn−∑k∈dom⁡g(nk)⁢g⁡kn-k+1
36 1 cv setvarm
37 36 35 cfv classwrecs⁡<ℕ0g∈V⟼⦋dom⁡g/n⦌xn−∑k∈dom⁡g(nk)⁢g⁡kn-k+1⁡m
38 1 3 2 4 37 cmpo classm∈ℕ0,x∈ℂ⟼wrecs⁡<ℕ0g∈V⟼⦋dom⁡g/n⦌xn−∑k∈dom⁡g(nk)⁢g⁡kn-k+1⁡m
39 0 38 wceq wffBernPoly=m∈ℕ0,x∈ℂ⟼wrecs⁡<ℕ0g∈V⟼⦋dom⁡g/n⦌xn−∑k∈dom⁡g(nk)⁢g⁡kn-k+1⁡m