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 ⁡ < ℕ 0 g ∈ V ⟼ ⦋ dom ⁡ g / n⦌ x n − ∑ k ∈ dom ⁡ g ( n k) ⁢ g ⁡ k n - k + 1 ⁡ m

Detailed syntax breakdown

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