Metamath Proof Explorer


Theorem bpoly0

Description: The value of the Bernoulli polynomials at zero. (Contributed by Scott Fenton, 16-May-2014)

Ref Expression
Assertion bpoly0 ( ๐‘‹ โˆˆ โ„‚ โ†’ ( 0 BernPoly ๐‘‹ ) = 1 )

Proof

Step Hyp Ref Expression
1 0nn0 โŠข 0 โˆˆ โ„•0
2 bpolyval โŠข ( ( 0 โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ โ„‚ ) โ†’ ( 0 BernPoly ๐‘‹ ) = ( ( ๐‘‹ โ†‘ 0 ) โˆ’ ฮฃ ๐‘˜ โˆˆ ( 0 ... ( 0 โˆ’ 1 ) ) ( ( 0 C ๐‘˜ ) ยท ( ( ๐‘˜ BernPoly ๐‘‹ ) / ( ( 0 โˆ’ ๐‘˜ ) + 1 ) ) ) ) )
3 1 2 mpan โŠข ( ๐‘‹ โˆˆ โ„‚ โ†’ ( 0 BernPoly ๐‘‹ ) = ( ( ๐‘‹ โ†‘ 0 ) โˆ’ ฮฃ ๐‘˜ โˆˆ ( 0 ... ( 0 โˆ’ 1 ) ) ( ( 0 C ๐‘˜ ) ยท ( ( ๐‘˜ BernPoly ๐‘‹ ) / ( ( 0 โˆ’ ๐‘˜ ) + 1 ) ) ) ) )
4 exp0 โŠข ( ๐‘‹ โˆˆ โ„‚ โ†’ ( ๐‘‹ โ†‘ 0 ) = 1 )
5 4 oveq1d โŠข ( ๐‘‹ โˆˆ โ„‚ โ†’ ( ( ๐‘‹ โ†‘ 0 ) โˆ’ ฮฃ ๐‘˜ โˆˆ ( 0 ... ( 0 โˆ’ 1 ) ) ( ( 0 C ๐‘˜ ) ยท ( ( ๐‘˜ BernPoly ๐‘‹ ) / ( ( 0 โˆ’ ๐‘˜ ) + 1 ) ) ) ) = ( 1 โˆ’ ฮฃ ๐‘˜ โˆˆ ( 0 ... ( 0 โˆ’ 1 ) ) ( ( 0 C ๐‘˜ ) ยท ( ( ๐‘˜ BernPoly ๐‘‹ ) / ( ( 0 โˆ’ ๐‘˜ ) + 1 ) ) ) ) )
6 risefall0lem โŠข ( 0 ... ( 0 โˆ’ 1 ) ) = โˆ…
7 6 sumeq1i โŠข ฮฃ ๐‘˜ โˆˆ ( 0 ... ( 0 โˆ’ 1 ) ) ( ( 0 C ๐‘˜ ) ยท ( ( ๐‘˜ BernPoly ๐‘‹ ) / ( ( 0 โˆ’ ๐‘˜ ) + 1 ) ) ) = ฮฃ ๐‘˜ โˆˆ โˆ… ( ( 0 C ๐‘˜ ) ยท ( ( ๐‘˜ BernPoly ๐‘‹ ) / ( ( 0 โˆ’ ๐‘˜ ) + 1 ) ) )
8 sum0 โŠข ฮฃ ๐‘˜ โˆˆ โˆ… ( ( 0 C ๐‘˜ ) ยท ( ( ๐‘˜ BernPoly ๐‘‹ ) / ( ( 0 โˆ’ ๐‘˜ ) + 1 ) ) ) = 0
9 7 8 eqtri โŠข ฮฃ ๐‘˜ โˆˆ ( 0 ... ( 0 โˆ’ 1 ) ) ( ( 0 C ๐‘˜ ) ยท ( ( ๐‘˜ BernPoly ๐‘‹ ) / ( ( 0 โˆ’ ๐‘˜ ) + 1 ) ) ) = 0
10 9 oveq2i โŠข ( 1 โˆ’ ฮฃ ๐‘˜ โˆˆ ( 0 ... ( 0 โˆ’ 1 ) ) ( ( 0 C ๐‘˜ ) ยท ( ( ๐‘˜ BernPoly ๐‘‹ ) / ( ( 0 โˆ’ ๐‘˜ ) + 1 ) ) ) ) = ( 1 โˆ’ 0 )
11 1m0e1 โŠข ( 1 โˆ’ 0 ) = 1
12 10 11 eqtri โŠข ( 1 โˆ’ ฮฃ ๐‘˜ โˆˆ ( 0 ... ( 0 โˆ’ 1 ) ) ( ( 0 C ๐‘˜ ) ยท ( ( ๐‘˜ BernPoly ๐‘‹ ) / ( ( 0 โˆ’ ๐‘˜ ) + 1 ) ) ) ) = 1
13 5 12 eqtrdi โŠข ( ๐‘‹ โˆˆ โ„‚ โ†’ ( ( ๐‘‹ โ†‘ 0 ) โˆ’ ฮฃ ๐‘˜ โˆˆ ( 0 ... ( 0 โˆ’ 1 ) ) ( ( 0 C ๐‘˜ ) ยท ( ( ๐‘˜ BernPoly ๐‘‹ ) / ( ( 0 โˆ’ ๐‘˜ ) + 1 ) ) ) ) = 1 )
14 3 13 eqtrd โŠข ( ๐‘‹ โˆˆ โ„‚ โ†’ ( 0 BernPoly ๐‘‹ ) = 1 )