MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-bpoly Structured version   Visualization version   GIF version

Definition df-bpoly 14983
Description: Define the Bernoulli polynomials. Here we use well-founded recursion to define the Bernoulli polynomials. This agrees with most textbook definitions, although explicit formulae 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
StepHypRef Expression
1 cbp 14982 . 2 class BernPoly
2 vm . . 3 setvar 𝑚
3 vx . . 3 setvar 𝑥
4 cn0 11493 . . 3 class 0
5 cc 10135 . . 3 class
62cv 1629 . . . 4 class 𝑚
7 clt 10275 . . . . 5 class <
8 vg . . . . . 6 setvar 𝑔
9 cvv 3349 . . . . . 6 class V
10 vn . . . . . . 7 setvar 𝑛
118cv 1629 . . . . . . . . 9 class 𝑔
1211cdm 5249 . . . . . . . 8 class dom 𝑔
13 chash 13320 . . . . . . . 8 class
1412, 13cfv 6031 . . . . . . 7 class (♯‘dom 𝑔)
153cv 1629 . . . . . . . . 9 class 𝑥
1610cv 1629 . . . . . . . . 9 class 𝑛
17 cexp 13066 . . . . . . . . 9 class
1815, 16, 17co 6792 . . . . . . . 8 class (𝑥𝑛)
19 vk . . . . . . . . . . . 12 setvar 𝑘
2019cv 1629 . . . . . . . . . . 11 class 𝑘
21 cbc 13292 . . . . . . . . . . 11 class C
2216, 20, 21co 6792 . . . . . . . . . 10 class (𝑛C𝑘)
2320, 11cfv 6031 . . . . . . . . . . 11 class (𝑔𝑘)
24 cmin 10467 . . . . . . . . . . . . 13 class
2516, 20, 24co 6792 . . . . . . . . . . . 12 class (𝑛𝑘)
26 c1 10138 . . . . . . . . . . . 12 class 1
27 caddc 10140 . . . . . . . . . . . 12 class +
2825, 26, 27co 6792 . . . . . . . . . . 11 class ((𝑛𝑘) + 1)
29 cdiv 10885 . . . . . . . . . . 11 class /
3023, 28, 29co 6792 . . . . . . . . . 10 class ((𝑔𝑘) / ((𝑛𝑘) + 1))
31 cmul 10142 . . . . . . . . . 10 class ·
3222, 30, 31co 6792 . . . . . . . . 9 class ((𝑛C𝑘) · ((𝑔𝑘) / ((𝑛𝑘) + 1)))
3312, 32, 19csu 14623 . . . . . . . 8 class Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔𝑘) / ((𝑛𝑘) + 1)))
3418, 33, 24co 6792 . . . . . . 7 class ((𝑥𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔𝑘) / ((𝑛𝑘) + 1))))
3510, 14, 34csb 3680 . . . . . 6 class (♯‘dom 𝑔) / 𝑛((𝑥𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔𝑘) / ((𝑛𝑘) + 1))))
368, 9, 35cmpt 4861 . . . . 5 class (𝑔 ∈ V ↦ (♯‘dom 𝑔) / 𝑛((𝑥𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔𝑘) / ((𝑛𝑘) + 1)))))
374, 7, 36cwrecs 7557 . . . 4 class wrecs( < , ℕ0, (𝑔 ∈ V ↦ (♯‘dom 𝑔) / 𝑛((𝑥𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔𝑘) / ((𝑛𝑘) + 1))))))
386, 37cfv 6031 . . 3 class (wrecs( < , ℕ0, (𝑔 ∈ V ↦ (♯‘dom 𝑔) / 𝑛((𝑥𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔𝑘) / ((𝑛𝑘) + 1))))))‘𝑚)
392, 3, 4, 5, 38cmpt2 6794 . 2 class (𝑚 ∈ ℕ0, 𝑥 ∈ ℂ ↦ (wrecs( < , ℕ0, (𝑔 ∈ V ↦ (♯‘dom 𝑔) / 𝑛((𝑥𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔𝑘) / ((𝑛𝑘) + 1))))))‘𝑚))
401, 39wceq 1630 1 wff BernPoly = (𝑚 ∈ ℕ0, 𝑥 ∈ ℂ ↦ (wrecs( < , ℕ0, (𝑔 ∈ V ↦ (♯‘dom 𝑔) / 𝑛((𝑥𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔𝑘) / ((𝑛𝑘) + 1))))))‘𝑚))
Colors of variables: wff setvar class
This definition is referenced by:  bpolylem  14984
  Copyright terms: Public domain W3C validator