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 ⊢ X ∈ ℂ → 1 BernPoly X = X − 1 2

Proof

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