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 15935
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.)
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 15934 . 2 class BernPoly
2 vm . . 3 setvar ๐‘š
3 vx . . 3 setvar ๐‘ฅ
4 cn0 12418 . . 3 class โ„•0
5 cc 11054 . . 3 class โ„‚
62cv 1541 . . . 4 class ๐‘š
7 clt 11194 . . . . 5 class <
8 vg . . . . . 6 setvar ๐‘”
9 cvv 3444 . . . . . 6 class V
10 vn . . . . . . 7 setvar ๐‘›
118cv 1541 . . . . . . . . 9 class ๐‘”
1211cdm 5634 . . . . . . . 8 class dom ๐‘”
13 chash 14236 . . . . . . . 8 class โ™ฏ
1412, 13cfv 6497 . . . . . . 7 class (โ™ฏโ€˜dom ๐‘”)
153cv 1541 . . . . . . . . 9 class ๐‘ฅ
1610cv 1541 . . . . . . . . 9 class ๐‘›
17 cexp 13973 . . . . . . . . 9 class โ†‘
1815, 16, 17co 7358 . . . . . . . 8 class (๐‘ฅโ†‘๐‘›)
19 vk . . . . . . . . . . . 12 setvar ๐‘˜
2019cv 1541 . . . . . . . . . . 11 class ๐‘˜
21 cbc 14208 . . . . . . . . . . 11 class C
2216, 20, 21co 7358 . . . . . . . . . 10 class (๐‘›C๐‘˜)
2320, 11cfv 6497 . . . . . . . . . . 11 class (๐‘”โ€˜๐‘˜)
24 cmin 11390 . . . . . . . . . . . . 13 class โˆ’
2516, 20, 24co 7358 . . . . . . . . . . . 12 class (๐‘› โˆ’ ๐‘˜)
26 c1 11057 . . . . . . . . . . . 12 class 1
27 caddc 11059 . . . . . . . . . . . 12 class +
2825, 26, 27co 7358 . . . . . . . . . . 11 class ((๐‘› โˆ’ ๐‘˜) + 1)
29 cdiv 11817 . . . . . . . . . . 11 class /
3023, 28, 29co 7358 . . . . . . . . . 10 class ((๐‘”โ€˜๐‘˜) / ((๐‘› โˆ’ ๐‘˜) + 1))
31 cmul 11061 . . . . . . . . . 10 class ยท
3222, 30, 31co 7358 . . . . . . . . 9 class ((๐‘›C๐‘˜) ยท ((๐‘”โ€˜๐‘˜) / ((๐‘› โˆ’ ๐‘˜) + 1)))
3312, 32, 19csu 15576 . . . . . . . 8 class ฮฃ๐‘˜ โˆˆ dom ๐‘”((๐‘›C๐‘˜) ยท ((๐‘”โ€˜๐‘˜) / ((๐‘› โˆ’ ๐‘˜) + 1)))
3418, 33, 24co 7358 . . . . . . 7 class ((๐‘ฅโ†‘๐‘›) โˆ’ ฮฃ๐‘˜ โˆˆ dom ๐‘”((๐‘›C๐‘˜) ยท ((๐‘”โ€˜๐‘˜) / ((๐‘› โˆ’ ๐‘˜) + 1))))
3510, 14, 34csb 3856 . . . . . 6 class โฆ‹(โ™ฏโ€˜dom ๐‘”) / ๐‘›โฆŒ((๐‘ฅโ†‘๐‘›) โˆ’ ฮฃ๐‘˜ โˆˆ dom ๐‘”((๐‘›C๐‘˜) ยท ((๐‘”โ€˜๐‘˜) / ((๐‘› โˆ’ ๐‘˜) + 1))))
368, 9, 35cmpt 5189 . . . . 5 class (๐‘” โˆˆ V โ†ฆ โฆ‹(โ™ฏโ€˜dom ๐‘”) / ๐‘›โฆŒ((๐‘ฅโ†‘๐‘›) โˆ’ ฮฃ๐‘˜ โˆˆ dom ๐‘”((๐‘›C๐‘˜) ยท ((๐‘”โ€˜๐‘˜) / ((๐‘› โˆ’ ๐‘˜) + 1)))))
374, 7, 36cwrecs 8243 . . . 4 class wrecs( < , โ„•0, (๐‘” โˆˆ V โ†ฆ โฆ‹(โ™ฏโ€˜dom ๐‘”) / ๐‘›โฆŒ((๐‘ฅโ†‘๐‘›) โˆ’ ฮฃ๐‘˜ โˆˆ dom ๐‘”((๐‘›C๐‘˜) ยท ((๐‘”โ€˜๐‘˜) / ((๐‘› โˆ’ ๐‘˜) + 1))))))
386, 37cfv 6497 . . 3 class (wrecs( < , โ„•0, (๐‘” โˆˆ V โ†ฆ โฆ‹(โ™ฏโ€˜dom ๐‘”) / ๐‘›โฆŒ((๐‘ฅโ†‘๐‘›) โˆ’ ฮฃ๐‘˜ โˆˆ dom ๐‘”((๐‘›C๐‘˜) ยท ((๐‘”โ€˜๐‘˜) / ((๐‘› โˆ’ ๐‘˜) + 1))))))โ€˜๐‘š)
392, 3, 4, 5, 38cmpo 7360 . 2 class (๐‘š โˆˆ โ„•0, ๐‘ฅ โˆˆ โ„‚ โ†ฆ (wrecs( < , โ„•0, (๐‘” โˆˆ V โ†ฆ โฆ‹(โ™ฏโ€˜dom ๐‘”) / ๐‘›โฆŒ((๐‘ฅโ†‘๐‘›) โˆ’ ฮฃ๐‘˜ โˆˆ dom ๐‘”((๐‘›C๐‘˜) ยท ((๐‘”โ€˜๐‘˜) / ((๐‘› โˆ’ ๐‘˜) + 1))))))โ€˜๐‘š))
401, 39wceq 1542 1 wff BernPoly = (๐‘š โˆˆ โ„•0, ๐‘ฅ โˆˆ โ„‚ โ†ฆ (wrecs( < , โ„•0, (๐‘” โˆˆ V โ†ฆ โฆ‹(โ™ฏโ€˜dom ๐‘”) / ๐‘›โฆŒ((๐‘ฅโ†‘๐‘›) โˆ’ ฮฃ๐‘˜ โˆˆ dom ๐‘”((๐‘›C๐‘˜) ยท ((๐‘”โ€˜๐‘˜) / ((๐‘› โˆ’ ๐‘˜) + 1))))))โ€˜๐‘š))
Colors of variables: wff setvar class
This definition is referenced by:  bpolylem  15936
  Copyright terms: Public domain W3C validator