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 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 ) ) )