Metamath Proof Explorer

Theorem bpoly0

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

Ref Expression
Assertion bpoly0 ⊢ X ∈ ℂ → 0 BernPoly X = 1

Proof

Step Hyp Ref Expression
1 0nn0 ⊢ 0 ∈ ℕ 0
2 bpolyval ⊢ 0 ∈ ℕ 0 ∧ X ∈ ℂ → 0 BernPoly X = X 0 − ∑ k = 0 0 − 1 ( 0 k) ⁢ k BernPoly X 0 - k + 1
3 1 2 mpan ⊢ X ∈ ℂ → 0 BernPoly X = X 0 − ∑ k = 0 0 − 1 ( 0 k) ⁢ k BernPoly X 0 - k + 1
4 exp0 ⊢ X ∈ ℂ → X 0 = 1
5 4 oveq1d ⊢ X ∈ ℂ → X 0 − ∑ k = 0 0 − 1 ( 0 k) ⁢ k BernPoly X 0 - k + 1 = 1 − ∑ k = 0 0 − 1 ( 0 k) ⁢ k BernPoly X 0 - k + 1
6 risefall0lem ⊢ 0 … 0 − 1 = ∅
7 6 sumeq1i ⊢ ∑ k = 0 0 − 1 ( 0 k) ⁢ k BernPoly X 0 - k + 1 = ∑ k ∈ ∅ ( 0 k) ⁢ k BernPoly X 0 - k + 1
8 sum0 ⊢ ∑ k ∈ ∅ ( 0 k) ⁢ k BernPoly X 0 - k + 1 = 0
9 7 8 eqtri ⊢ ∑ k = 0 0 − 1 ( 0 k) ⁢ k BernPoly X 0 - k + 1 = 0
10 9 oveq2i ⊢ 1 − ∑ k = 0 0 − 1 ( 0 k) ⁢ k BernPoly X 0 - k + 1 = 1 − 0
11 1m0e1 ⊢ 1 − 0 = 1
12 10 11 eqtri ⊢ 1 − ∑ k = 0 0 − 1 ( 0 k) ⁢ k BernPoly X 0 - k + 1 = 1
13 5 12 eqtrdi ⊢ X ∈ ℂ → X 0 − ∑ k = 0 0 − 1 ( 0 k) ⁢ k BernPoly X 0 - k + 1 = 1
14 3 13 eqtrd ⊢ X ∈ ℂ → 0 BernPoly X = 1