bpoly0

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

		Ref	Expression
	Assertion	bpoly0	$⊢ X \in ℂ \to 0 BernPoly X = 1$

Step	Hyp	Ref	Expression
1		0nn0	$⊢ 0 \in ℕ_{0}$
2		bpolyval	$⊢ (0 \in ℕ_{0} \land X \in ℂ) \to 0 BernPoly X = X^{0} - \sum_{k = 0}^{0 - 1} (\binom{0}{k}) (\frac{k BernPoly X}{0 - k + 1})$
3	1 2	mpan	$⊢ X \in ℂ \to 0 BernPoly X = X^{0} - \sum_{k = 0}^{0 - 1} (\binom{0}{k}) (\frac{k BernPoly X}{0 - k + 1})$
4		exp0	$⊢ X \in ℂ \to X^{0} = 1$
5	4	oveq1d	$⊢ X \in ℂ \to X^{0} - \sum_{k = 0}^{0 - 1} (\binom{0}{k}) (\frac{k BernPoly X}{0 - k + 1}) = 1 - \sum_{k = 0}^{0 - 1} (\binom{0}{k}) (\frac{k BernPoly X}{0 - k + 1})$
6		risefall0lem	$⊢ (0 \dots 0 - 1) = \emptyset$
7	6	sumeq1i	$⊢ \sum_{k = 0}^{0 - 1} (\binom{0}{k}) (\frac{k BernPoly X}{0 - k + 1}) = \sum_{k \in \emptyset} (\binom{0}{k}) (\frac{k BernPoly X}{0 - k + 1})$
8		sum0	$⊢ \sum_{k \in \emptyset} (\binom{0}{k}) (\frac{k BernPoly X}{0 - k + 1}) = 0$
9	7 8	eqtri	$⊢ \sum_{k = 0}^{0 - 1} (\binom{0}{k}) (\frac{k BernPoly X}{0 - k + 1}) = 0$
10	9	oveq2i	$⊢ 1 - \sum_{k = 0}^{0 - 1} (\binom{0}{k}) (\frac{k BernPoly X}{0 - k + 1}) = 1 - 0$
11		1m0e1	$⊢ 1 - 0 = 1$
12	10 11	eqtri	$⊢ 1 - \sum_{k = 0}^{0 - 1} (\binom{0}{k}) (\frac{k BernPoly X}{0 - k + 1}) = 1$
13	5 12	eqtrdi	$⊢ X \in ℂ \to X^{0} - \sum_{k = 0}^{0 - 1} (\binom{0}{k}) (\frac{k BernPoly X}{0 - k + 1}) = 1$
14	3 13	eqtrd	$⊢ X \in ℂ \to 0 BernPoly X = 1$

Metamath Proof Explorer