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 = ( 𝑚 ∈ ℕ0 , 𝑥 ∈ ℂ ↦ ( wrecs ( < , ℕ0 , ( 𝑔 ∈ V ↦ ⦋ ( ♯ ‘ dom 𝑔 ) / 𝑛 ⦌ ( ( 𝑥 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) ) ) ‘ 𝑚 ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cbp ⊢ BernPoly
1 vm ⊢ 𝑚
2 cn0 ⊢ ℕ0
3 vx ⊢ 𝑥
4 cc ⊢ ℂ
5 clt ⊢ <
6 vg ⊢ 𝑔
7 cvv ⊢ V
8 chash ⊢ ♯
9 6 cv ⊢ 𝑔
10 9 cdm ⊢ dom 𝑔
11 10 8 cfv ⊢ ( ♯ ‘ dom 𝑔 )
12 vn ⊢ 𝑛
13 3 cv ⊢ 𝑥
14 cexp ⊢ ↑
15 12 cv ⊢ 𝑛
16 13 15 14 co ⊢ ( 𝑥 ↑ 𝑛 )
17 cmin ⊢ −
18 vk ⊢ 𝑘
19 cbc ⊢ C
20 18 cv ⊢ 𝑘
21 15 20 19 co ⊢ ( 𝑛 C 𝑘 )
22 cmul ⊢ ·
23 20 9 cfv ⊢ ( 𝑔 ‘ 𝑘 )
24 cdiv ⊢ /
25 15 20 17 co ⊢ ( 𝑛 − 𝑘 )
26 caddc ⊢ +
27 c1 ⊢ 1
28 25 27 26 co ⊢ ( ( 𝑛 − 𝑘 ) + 1 )
29 23 28 24 co ⊢ ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) )
30 21 29 22 co ⊢ ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) )
31 10 30 18 csu ⊢ Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) )
32 16 31 17 co ⊢ ( ( 𝑥 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) )
33 12 11 32 csb ⊢ ⦋ ( ♯ ‘ dom 𝑔 ) / 𝑛 ⦌ ( ( 𝑥 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) )
34 6 7 33 cmpt ⊢ ( 𝑔 ∈ V ↦ ⦋ ( ♯ ‘ dom 𝑔 ) / 𝑛 ⦌ ( ( 𝑥 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) )
35 2 5 34 cwrecs ⊢ wrecs ( < , ℕ0 , ( 𝑔 ∈ V ↦ ⦋ ( ♯ ‘ dom 𝑔 ) / 𝑛 ⦌ ( ( 𝑥 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) ) )
36 1 cv ⊢ 𝑚
37 36 35 cfv ⊢ ( wrecs ( < , ℕ0 , ( 𝑔 ∈ V ↦ ⦋ ( ♯ ‘ dom 𝑔 ) / 𝑛 ⦌ ( ( 𝑥 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) ) ) ‘ 𝑚 )
38 1 3 2 4 37 cmpo ⊢ ( 𝑚 ∈ ℕ0 , 𝑥 ∈ ℂ ↦ ( wrecs ( < , ℕ0 , ( 𝑔 ∈ V ↦ ⦋ ( ♯ ‘ dom 𝑔 ) / 𝑛 ⦌ ( ( 𝑥 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) ) ) ‘ 𝑚 ) )
39 0 38 wceq ⊢ BernPoly = ( 𝑚 ∈ ℕ0 , 𝑥 ∈ ℂ ↦ ( wrecs ( < , ℕ0 , ( 𝑔 ∈ V ↦ ⦋ ( ♯ ‘ dom 𝑔 ) / 𝑛 ⦌ ( ( 𝑥 ↑ 𝑛 ) − Σ 𝑘 ∈ dom 𝑔 ( ( 𝑛 C 𝑘 ) · ( ( 𝑔 ‘ 𝑘 ) / ( ( 𝑛 − 𝑘 ) + 1 ) ) ) ) ) ) ‘ 𝑚 ) )