Theorem bpoly1

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

	Ref	Expression
Assertion	bpoly1	⊢ ( 𝑋 ∈ ℂ → ( 1 BernPoly 𝑋 ) = ( 𝑋 − ( 1 / 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		1nn0	⊢ 1 ∈ ℕ0
2		bpolyval	⊢ ( ( 1 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( 1 BernPoly 𝑋 ) = ( ( 𝑋 ↑ 1 ) − Σ 𝑘 ∈ ( 0 ... ( 1 − 1 ) ) ( ( 1 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 1 − 𝑘 ) + 1 ) ) ) ) )
3	1 2	mpan	⊢ ( 𝑋 ∈ ℂ → ( 1 BernPoly 𝑋 ) = ( ( 𝑋 ↑ 1 ) − Σ 𝑘 ∈ ( 0 ... ( 1 − 1 ) ) ( ( 1 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 1 − 𝑘 ) + 1 ) ) ) ) )
4		exp1	⊢ ( 𝑋 ∈ ℂ → ( 𝑋 ↑ 1 ) = 𝑋 )
5		1m1e0	⊢ ( 1 − 1 ) = 0
6	5	oveq2i	⊢ ( 0 ... ( 1 − 1 ) ) = ( 0 ... 0 )
7	6	sumeq1i	⊢ Σ 𝑘 ∈ ( 0 ... ( 1 − 1 ) ) ( ( 1 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 1 − 𝑘 ) + 1 ) ) ) = Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 1 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 1 − 𝑘 ) + 1 ) ) )
8		0z	⊢ 0 ∈ ℤ
9		bpoly0	⊢ ( 𝑋 ∈ ℂ → ( 0 BernPoly 𝑋 ) = 1 )
10	9	oveq1d	⊢ ( 𝑋 ∈ ℂ → ( ( 0 BernPoly 𝑋 ) / 2 ) = ( 1 / 2 ) )
11	10	oveq2d	⊢ ( 𝑋 ∈ ℂ → ( 1 · ( ( 0 BernPoly 𝑋 ) / 2 ) ) = ( 1 · ( 1 / 2 ) ) )
12		halfcn	⊢ ( 1 / 2 ) ∈ ℂ
13	12	mullidi	⊢ ( 1 · ( 1 / 2 ) ) = ( 1 / 2 )
14	11 13	eqtrdi	⊢ ( 𝑋 ∈ ℂ → ( 1 · ( ( 0 BernPoly 𝑋 ) / 2 ) ) = ( 1 / 2 ) )
15	14 12	eqeltrdi	⊢ ( 𝑋 ∈ ℂ → ( 1 · ( ( 0 BernPoly 𝑋 ) / 2 ) ) ∈ ℂ )
16		oveq2	⊢ ( 𝑘 = 0 → ( 1 C 𝑘 ) = ( 1 C 0 ) )
17		bcn0	⊢ ( 1 ∈ ℕ0 → ( 1 C 0 ) = 1 )
18	1 17	ax-mp	⊢ ( 1 C 0 ) = 1
19	16 18	eqtrdi	⊢ ( 𝑘 = 0 → ( 1 C 𝑘 ) = 1 )
20		oveq1	⊢ ( 𝑘 = 0 → ( 𝑘 BernPoly 𝑋 ) = ( 0 BernPoly 𝑋 ) )
21		oveq2	⊢ ( 𝑘 = 0 → ( 1 − 𝑘 ) = ( 1 − 0 ) )
22		1m0e1	⊢ ( 1 − 0 ) = 1
23	21 22	eqtrdi	⊢ ( 𝑘 = 0 → ( 1 − 𝑘 ) = 1 )
24	23	oveq1d	⊢ ( 𝑘 = 0 → ( ( 1 − 𝑘 ) + 1 ) = ( 1 + 1 ) )
25		df-2	⊢ 2 = ( 1 + 1 )
26	24 25	eqtr4di	⊢ ( 𝑘 = 0 → ( ( 1 − 𝑘 ) + 1 ) = 2 )
27	20 26	oveq12d	⊢ ( 𝑘 = 0 → ( ( 𝑘 BernPoly 𝑋 ) / ( ( 1 − 𝑘 ) + 1 ) ) = ( ( 0 BernPoly 𝑋 ) / 2 ) )
28	19 27	oveq12d	⊢ ( 𝑘 = 0 → ( ( 1 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 1 − 𝑘 ) + 1 ) ) ) = ( 1 · ( ( 0 BernPoly 𝑋 ) / 2 ) ) )
29	28	fsum1	⊢ ( ( 0 ∈ ℤ ∧ ( 1 · ( ( 0 BernPoly 𝑋 ) / 2 ) ) ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 1 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 1 − 𝑘 ) + 1 ) ) ) = ( 1 · ( ( 0 BernPoly 𝑋 ) / 2 ) ) )
30	8 15 29	sylancr	⊢ ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 1 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 1 − 𝑘 ) + 1 ) ) ) = ( 1 · ( ( 0 BernPoly 𝑋 ) / 2 ) ) )
31	30 14	eqtrd	⊢ ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 1 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 1 − 𝑘 ) + 1 ) ) ) = ( 1 / 2 ) )
32	7 31	eqtrid	⊢ ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 0 ... ( 1 − 1 ) ) ( ( 1 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 1 − 𝑘 ) + 1 ) ) ) = ( 1 / 2 ) )
33	4 32	oveq12d	⊢ ( 𝑋 ∈ ℂ → ( ( 𝑋 ↑ 1 ) − Σ 𝑘 ∈ ( 0 ... ( 1 − 1 ) ) ( ( 1 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 1 − 𝑘 ) + 1 ) ) ) ) = ( 𝑋 − ( 1 / 2 ) ) )
34	3 33	eqtrd	⊢ ( 𝑋 ∈ ℂ → ( 1 BernPoly 𝑋 ) = ( 𝑋 − ( 1 / 2 ) ) )