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

Definition df-bpoly 14112
 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 wrecs
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-bpoly
StepHypRef Expression
1 cbp 14111 . 2 BernPoly
2 vm . . 3
3 vx . . 3
4 cn0 10876 . . 3
5 cc 9542 . . 3
62cv 1445 . . . 4
7 clt 9680 . . . . 5
8 vg . . . . . 6
9 cvv 3047 . . . . . 6
10 vn . . . . . . 7
118cv 1445 . . . . . . . . 9
1211cdm 4837 . . . . . . . 8
13 chash 12522 . . . . . . . 8
1412, 13cfv 5585 . . . . . . 7
153cv 1445 . . . . . . . . 9
1610cv 1445 . . . . . . . . 9
17 cexp 12279 . . . . . . . . 9
1815, 16, 17co 6295 . . . . . . . 8
19 vk . . . . . . . . . . . 12
2019cv 1445 . . . . . . . . . . 11
21 cbc 12494 . . . . . . . . . . 11
2216, 20, 21co 6295 . . . . . . . . . 10
2320, 11cfv 5585 . . . . . . . . . . 11
24 cmin 9865 . . . . . . . . . . . . 13
2516, 20, 24co 6295 . . . . . . . . . . . 12
26 c1 9545 . . . . . . . . . . . 12
27 caddc 9547 . . . . . . . . . . . 12
2825, 26, 27co 6295 . . . . . . . . . . 11
29 cdiv 10276 . . . . . . . . . . 11
3023, 28, 29co 6295 . . . . . . . . . 10
31 cmul 9549 . . . . . . . . . 10
3222, 30, 31co 6295 . . . . . . . . 9
3312, 32, 19csu 13764 . . . . . . . 8
3418, 33, 24co 6295 . . . . . . 7
3510, 14, 34csb 3365 . . . . . 6
368, 9, 35cmpt 4464 . . . . 5
374, 7, 36cwrecs 7032 . . . 4 wrecs
386, 37cfv 5585 . . 3 wrecs
392, 3, 4, 5, 38cmpt2 6297 . 2 wrecs
401, 39wceq 1446 1 BernPoly wrecs
 Colors of variables: wff setvar class This definition is referenced by:  bpolylem  14113
 Copyright terms: Public domain W3C validator