bpoly1

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

		Ref	Expression
	Assertion	bpoly1	$⊢ X \in ℂ \to 1 BernPoly X = X - (\frac{1}{2})$

Proof

Step	Hyp	Ref	Expression
1		1nn0	$⊢ 1 \in ℕ_{0}$
2		bpolyval	$⊢ (1 \in ℕ_{0} \land X \in ℂ) \to 1 BernPoly X = X^{1} - \sum_{k = 0}^{1 - 1} (\binom{1}{k}) (\frac{k BernPoly X}{1 - k + 1})$
3	1 2	mpan	$⊢ X \in ℂ \to 1 BernPoly X = X^{1} - \sum_{k = 0}^{1 - 1} (\binom{1}{k}) (\frac{k BernPoly X}{1 - k + 1})$
4		exp1	$⊢ X \in ℂ \to X^{1} = X$
5		1m1e0	$⊢ 1 - 1 = 0$
6	5	oveq2i	$⊢ (0 \dots 1 - 1) = (0 \dots 0)$
7	6	sumeq1i	$⊢ \sum_{k = 0}^{1 - 1} (\binom{1}{k}) (\frac{k BernPoly X}{1 - k + 1}) = \sum_{k = 0}^{0} (\binom{1}{k}) (\frac{k BernPoly X}{1 - k + 1})$
8		0z	$⊢ 0 \in ℤ$
9		bpoly0	$⊢ X \in ℂ \to 0 BernPoly X = 1$
10	9	oveq1d	$⊢ X \in ℂ \to \frac{0 BernPoly X}{2} = \frac{1}{2}$
11	10	oveq2d	$⊢ X \in ℂ \to 1 (\frac{0 BernPoly X}{2}) = 1 (\frac{1}{2})$
12		halfcn	$⊢ \frac{1}{2} \in ℂ$
13	12	mullidi	$⊢ 1 (\frac{1}{2}) = \frac{1}{2}$
14	11 13	eqtrdi	$⊢ X \in ℂ \to 1 (\frac{0 BernPoly X}{2}) = \frac{1}{2}$
15	14 12	eqeltrdi	$⊢ X \in ℂ \to 1 (\frac{0 BernPoly X}{2}) \in ℂ$
16		oveq2	$⊢ k = 0 \to (\binom{1}{k}) = (\binom{1}{0})$
17		bcn0	$⊢ 1 \in ℕ_{0} \to (\binom{1}{0}) = 1$
18	1 17	ax-mp	$⊢ (\binom{1}{0}) = 1$
19	16 18	eqtrdi	$⊢ k = 0 \to (\binom{1}{k}) = 1$
20		oveq1	$⊢ k = 0 \to k BernPoly X = 0 BernPoly X$
21		oveq2	$⊢ k = 0 \to 1 - k = 1 - 0$
22		1m0e1	$⊢ 1 - 0 = 1$
23	21 22	eqtrdi	$⊢ k = 0 \to 1 - k = 1$
24	23	oveq1d	$⊢ k = 0 \to 1 - k + 1 = 1 + 1$
25		df-2	$⊢ 2 = 1 + 1$
26	24 25	eqtr4di	$⊢ k = 0 \to 1 - k + 1 = 2$
27	20 26	oveq12d	$⊢ k = 0 \to \frac{k BernPoly X}{1 - k + 1} = \frac{0 BernPoly X}{2}$
28	19 27	oveq12d	$⊢ k = 0 \to (\binom{1}{k}) (\frac{k BernPoly X}{1 - k + 1}) = 1 (\frac{0 BernPoly X}{2})$
29	28	fsum1	$⊢ (0 \in ℤ \land 1 (\frac{0 BernPoly X}{2}) \in ℂ) \to \sum_{k = 0}^{0} (\binom{1}{k}) (\frac{k BernPoly X}{1 - k + 1}) = 1 (\frac{0 BernPoly X}{2})$
30	8 15 29	sylancr	$⊢ X \in ℂ \to \sum_{k = 0}^{0} (\binom{1}{k}) (\frac{k BernPoly X}{1 - k + 1}) = 1 (\frac{0 BernPoly X}{2})$
31	30 14	eqtrd	$⊢ X \in ℂ \to \sum_{k = 0}^{0} (\binom{1}{k}) (\frac{k BernPoly X}{1 - k + 1}) = \frac{1}{2}$
32	7 31	eqtrid	$⊢ X \in ℂ \to \sum_{k = 0}^{1 - 1} (\binom{1}{k}) (\frac{k BernPoly X}{1 - k + 1}) = \frac{1}{2}$
33	4 32	oveq12d	$⊢ X \in ℂ \to X^{1} - \sum_{k = 0}^{1 - 1} (\binom{1}{k}) (\frac{k BernPoly X}{1 - k + 1}) = X - (\frac{1}{2})$
34	3 33	eqtrd	$⊢ X \in ℂ \to 1 BernPoly X = X - (\frac{1}{2})$

Metamath Proof Explorer

Theorem bpoly1

Proof