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 )