Metamath Proof Explorer

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 mulid2i ⊢ ( 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 syl5eq ⊢ ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 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 ) ) )