Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bpoly Structured version   Unicode version

Definition df-bpoly 26098
 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 26097 . 2 BernPoly
2 vm . . 3
3 vx . . 3
4 cn0 10226 . . 3
5 cc 8993 . . 3
62cv 1652 . . . 4
7 clt 9125 . . . . 5
8 vg . . . . . 6
9 cvv 2958 . . . . . 6
10 vn . . . . . . 7
118cv 1652 . . . . . . . . 9
1211cdm 4881 . . . . . . . 8
13 chash 11623 . . . . . . . 8
1412, 13cfv 5457 . . . . . . 7
153cv 1652 . . . . . . . . 9
1610cv 1652 . . . . . . . . 9
17 cexp 11387 . . . . . . . . 9
1815, 16, 17co 6084 . . . . . . . 8
19 vk . . . . . . . . . . . 12
2019cv 1652 . . . . . . . . . . 11
21 cbc 11598 . . . . . . . . . . 11
2216, 20, 21co 6084 . . . . . . . . . 10
2320, 11cfv 5457 . . . . . . . . . . 11
24 cmin 9296 . . . . . . . . . . . . 13
2516, 20, 24co 6084 . . . . . . . . . . . 12
26 c1 8996 . . . . . . . . . . . 12
27 caddc 8998 . . . . . . . . . . . 12
2825, 26, 27co 6084 . . . . . . . . . . 11
29 cdiv 9682 . . . . . . . . . . 11
3023, 28, 29co 6084 . . . . . . . . . 10
31 cmul 9000 . . . . . . . . . 10
3222, 30, 31co 6084 . . . . . . . . 9
3312, 32, 19csu 12484 . . . . . . . 8
3418, 33, 24co 6084 . . . . . . 7
3510, 14, 34csb 3253 . . . . . 6
368, 9, 35cmpt 4269 . . . . 5
374, 7, 36cwrecs 25535 . . . 4 wrecs
386, 37cfv 5457 . . 3 wrecs
392, 3, 4, 5, 38cmpt2 6086 . 2 wrecs
401, 39wceq 1653 1 BernPoly wrecs
 Colors of variables: wff set class This definition is referenced by:  bpolylem  26099
 Copyright terms: Public domain W3C validator