bpoly2

Description: The Bernoulli polynomials at two. (Contributed by Scott Fenton, 8-Jul-2015)

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

Proof

Step	Hyp	Ref	Expression
1		2nn0	$⊢ 2 \in ℕ_{0}$
2		bpolyval	$⊢ (2 \in ℕ_{0} \land X \in ℂ) \to 2 BernPoly X = X^{2} - \sum_{k = 0}^{2 - 1} (\binom{2}{k}) (\frac{k BernPoly X}{2 - k + 1})$
3	1 2	mpan	$⊢ X \in ℂ \to 2 BernPoly X = X^{2} - \sum_{k = 0}^{2 - 1} (\binom{2}{k}) (\frac{k BernPoly X}{2 - k + 1})$
4		2m1e1	$⊢ 2 - 1 = 1$
5		0p1e1	$⊢ 0 + 1 = 1$
6	4 5	eqtr4i	$⊢ 2 - 1 = 0 + 1$
7	6	oveq2i	$⊢ (0 \dots 2 - 1) = (0 \dots 0 + 1)$
8	7	sumeq1i	$⊢ \sum_{k = 0}^{2 - 1} (\binom{2}{k}) (\frac{k BernPoly X}{2 - k + 1}) = \sum_{k = 0}^{0 + 1} (\binom{2}{k}) (\frac{k BernPoly X}{2 - k + 1})$
9		0nn0	$⊢ 0 \in ℕ_{0}$
10		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
11	9 10	eleqtri	$⊢ 0 \in ℤ_{\geq 0}$
12	11	a1i	$⊢ X \in ℂ \to 0 \in ℤ_{\geq 0}$
13		0z	$⊢ 0 \in ℤ$
14		fzpr	$⊢ 0 \in ℤ \to (0 \dots 0 + 1) = \{0, 0 + 1\}$
15	13 14	ax-mp	$⊢ (0 \dots 0 + 1) = \{0, 0 + 1\}$
16	15	eleq2i	$⊢ k \in (0 \dots 0 + 1) \leftrightarrow k \in \{0, 0 + 1\}$
17		vex	$⊢ k \in V$
18	17	elpr	$⊢ k \in \{0, 0 + 1\} \leftrightarrow (k = 0 \lor k = 0 + 1)$
19	16 18	bitri	$⊢ k \in (0 \dots 0 + 1) \leftrightarrow (k = 0 \lor k = 0 + 1)$
20		oveq2	$⊢ k = 0 \to (\binom{2}{k}) = (\binom{2}{0})$
21		bcn0	$⊢ 2 \in ℕ_{0} \to (\binom{2}{0}) = 1$
22	1 21	ax-mp	$⊢ (\binom{2}{0}) = 1$
23	20 22	eqtrdi	$⊢ k = 0 \to (\binom{2}{k}) = 1$
24		oveq1	$⊢ k = 0 \to k BernPoly X = 0 BernPoly X$
25		oveq2	$⊢ k = 0 \to 2 - k = 2 - 0$
26	25	oveq1d	$⊢ k = 0 \to 2 - k + 1 = 2 - 0 + 1$
27		2cn	$⊢ 2 \in ℂ$
28	27	subid1i	$⊢ 2 - 0 = 2$
29	28	oveq1i	$⊢ 2 - 0 + 1 = 2 + 1$
30		df-3	$⊢ 3 = 2 + 1$
31	29 30	eqtr4i	$⊢ 2 - 0 + 1 = 3$
32	26 31	eqtrdi	$⊢ k = 0 \to 2 - k + 1 = 3$
33	24 32	oveq12d	$⊢ k = 0 \to \frac{k BernPoly X}{2 - k + 1} = \frac{0 BernPoly X}{3}$
34	23 33	oveq12d	$⊢ k = 0 \to (\binom{2}{k}) (\frac{k BernPoly X}{2 - k + 1}) = 1 (\frac{0 BernPoly X}{3})$
35		bpoly0	$⊢ X \in ℂ \to 0 BernPoly X = 1$
36	35	oveq1d	$⊢ X \in ℂ \to \frac{0 BernPoly X}{3} = \frac{1}{3}$
37	36	oveq2d	$⊢ X \in ℂ \to 1 (\frac{0 BernPoly X}{3}) = 1 (\frac{1}{3})$
38		3cn	$⊢ 3 \in ℂ$
39		3ne0	$⊢ 3 \neq 0$
40	38 39	reccli	$⊢ \frac{1}{3} \in ℂ$
41	40	mullidi	$⊢ 1 (\frac{1}{3}) = \frac{1}{3}$
42	37 41	eqtrdi	$⊢ X \in ℂ \to 1 (\frac{0 BernPoly X}{3}) = \frac{1}{3}$
43	34 42	sylan9eqr	$⊢ (X \in ℂ \land k = 0) \to (\binom{2}{k}) (\frac{k BernPoly X}{2 - k + 1}) = \frac{1}{3}$
44	43 40	eqeltrdi	$⊢ (X \in ℂ \land k = 0) \to (\binom{2}{k}) (\frac{k BernPoly X}{2 - k + 1}) \in ℂ$
45	5	eqeq2i	$⊢ k = 0 + 1 \leftrightarrow k = 1$
46		oveq2	$⊢ k = 1 \to (\binom{2}{k}) = (\binom{2}{1})$
47		bcn1	$⊢ 2 \in ℕ_{0} \to (\binom{2}{1}) = 2$
48	1 47	ax-mp	$⊢ (\binom{2}{1}) = 2$
49	46 48	eqtrdi	$⊢ k = 1 \to (\binom{2}{k}) = 2$
50		oveq1	$⊢ k = 1 \to k BernPoly X = 1 BernPoly X$
51		oveq2	$⊢ k = 1 \to 2 - k = 2 - 1$
52	51	oveq1d	$⊢ k = 1 \to 2 - k + 1 = 2 - 1 + 1$
53		ax-1cn	$⊢ 1 \in ℂ$
54		npcan	$⊢ (2 \in ℂ \land 1 \in ℂ) \to 2 - 1 + 1 = 2$
55	27 53 54	mp2an	$⊢ 2 - 1 + 1 = 2$
56	52 55	eqtrdi	$⊢ k = 1 \to 2 - k + 1 = 2$
57	50 56	oveq12d	$⊢ k = 1 \to \frac{k BernPoly X}{2 - k + 1} = \frac{1 BernPoly X}{2}$
58	49 57	oveq12d	$⊢ k = 1 \to (\binom{2}{k}) (\frac{k BernPoly X}{2 - k + 1}) = 2 (\frac{1 BernPoly X}{2})$
59	45 58	sylbi	$⊢ k = 0 + 1 \to (\binom{2}{k}) (\frac{k BernPoly X}{2 - k + 1}) = 2 (\frac{1 BernPoly X}{2})$
60		bpoly1	$⊢ X \in ℂ \to 1 BernPoly X = X - (\frac{1}{2})$
61	60	oveq1d	$⊢ X \in ℂ \to \frac{1 BernPoly X}{2} = \frac{X - (\frac{1}{2})}{2}$
62	61	oveq2d	$⊢ X \in ℂ \to 2 (\frac{1 BernPoly X}{2}) = 2 (\frac{X - (\frac{1}{2})}{2})$
63		halfcn	$⊢ \frac{1}{2} \in ℂ$
64		subcl	$⊢ (X \in ℂ \land \frac{1}{2} \in ℂ) \to X - (\frac{1}{2}) \in ℂ$
65	63 64	mpan2	$⊢ X \in ℂ \to X - (\frac{1}{2}) \in ℂ$
66		2ne0	$⊢ 2 \neq 0$
67		divcan2	$⊢ (X - (\frac{1}{2}) \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to 2 (\frac{X - (\frac{1}{2})}{2}) = X - (\frac{1}{2})$
68	27 66 67	mp3an23	$⊢ X - (\frac{1}{2}) \in ℂ \to 2 (\frac{X - (\frac{1}{2})}{2}) = X - (\frac{1}{2})$
69	65 68	syl	$⊢ X \in ℂ \to 2 (\frac{X - (\frac{1}{2})}{2}) = X - (\frac{1}{2})$
70	62 69	eqtrd	$⊢ X \in ℂ \to 2 (\frac{1 BernPoly X}{2}) = X - (\frac{1}{2})$
71	59 70	sylan9eqr	$⊢ (X \in ℂ \land k = 0 + 1) \to (\binom{2}{k}) (\frac{k BernPoly X}{2 - k + 1}) = X - (\frac{1}{2})$
72	65	adantr	$⊢ (X \in ℂ \land k = 0 + 1) \to X - (\frac{1}{2}) \in ℂ$
73	71 72	eqeltrd	$⊢ (X \in ℂ \land k = 0 + 1) \to (\binom{2}{k}) (\frac{k BernPoly X}{2 - k + 1}) \in ℂ$
74	44 73	jaodan	$⊢ (X \in ℂ \land (k = 0 \lor k = 0 + 1)) \to (\binom{2}{k}) (\frac{k BernPoly X}{2 - k + 1}) \in ℂ$
75	19 74	sylan2b	$⊢ (X \in ℂ \land k \in (0 \dots 0 + 1)) \to (\binom{2}{k}) (\frac{k BernPoly X}{2 - k + 1}) \in ℂ$
76	12 75 59	fsump1	$⊢ X \in ℂ \to \sum_{k = 0}^{0 + 1} (\binom{2}{k}) (\frac{k BernPoly X}{2 - k + 1}) = \sum_{k = 0}^{0} (\binom{2}{k}) (\frac{k BernPoly X}{2 - k + 1}) + 2 (\frac{1 BernPoly X}{2})$
77	42 40	eqeltrdi	$⊢ X \in ℂ \to 1 (\frac{0 BernPoly X}{3}) \in ℂ$
78	34	fsum1	$⊢ (0 \in ℤ \land 1 (\frac{0 BernPoly X}{3}) \in ℂ) \to \sum_{k = 0}^{0} (\binom{2}{k}) (\frac{k BernPoly X}{2 - k + 1}) = 1 (\frac{0 BernPoly X}{3})$
79	13 77 78	sylancr	$⊢ X \in ℂ \to \sum_{k = 0}^{0} (\binom{2}{k}) (\frac{k BernPoly X}{2 - k + 1}) = 1 (\frac{0 BernPoly X}{3})$
80	79 42	eqtrd	$⊢ X \in ℂ \to \sum_{k = 0}^{0} (\binom{2}{k}) (\frac{k BernPoly X}{2 - k + 1}) = \frac{1}{3}$
81	80 70	oveq12d	$⊢ X \in ℂ \to \sum_{k = 0}^{0} (\binom{2}{k}) (\frac{k BernPoly X}{2 - k + 1}) + 2 (\frac{1 BernPoly X}{2}) = (\frac{1}{3}) + X - (\frac{1}{2})$
82	76 81	eqtrd	$⊢ X \in ℂ \to \sum_{k = 0}^{0 + 1} (\binom{2}{k}) (\frac{k BernPoly X}{2 - k + 1}) = (\frac{1}{3}) + X - (\frac{1}{2})$
83		addsub12	$⊢ (\frac{1}{3} \in ℂ \land X \in ℂ \land \frac{1}{2} \in ℂ) \to (\frac{1}{3}) + X - (\frac{1}{2}) = X + (\frac{1}{3}) - (\frac{1}{2})$
84	40 63 83	mp3an13	$⊢ X \in ℂ \to (\frac{1}{3}) + X - (\frac{1}{2}) = X + (\frac{1}{3}) - (\frac{1}{2})$
85	63 40	negsubdi2i	$⊢ - ((\frac{1}{2}) - (\frac{1}{3})) = (\frac{1}{3}) - (\frac{1}{2})$
86		halfthird	$⊢ (\frac{1}{2}) - (\frac{1}{3}) = \frac{1}{6}$
87	86	negeqi	$⊢ - ((\frac{1}{2}) - (\frac{1}{3})) = - \frac{1}{6}$
88	85 87	eqtr3i	$⊢ (\frac{1}{3}) - (\frac{1}{2}) = - \frac{1}{6}$
89	88	oveq2i	$⊢ X + (\frac{1}{3}) - (\frac{1}{2}) = X + (- \frac{1}{6})$
90	84 89	eqtrdi	$⊢ X \in ℂ \to (\frac{1}{3}) + X - (\frac{1}{2}) = X + (- \frac{1}{6})$
91		6cn	$⊢ 6 \in ℂ$
92		6re	$⊢ 6 \in ℝ$
93		6pos	$⊢ 0 < 6$
94	92 93	gt0ne0ii	$⊢ 6 \neq 0$
95	91 94	reccli	$⊢ \frac{1}{6} \in ℂ$
96		negsub	$⊢ (X \in ℂ \land \frac{1}{6} \in ℂ) \to X + (- \frac{1}{6}) = X - (\frac{1}{6})$
97	95 96	mpan2	$⊢ X \in ℂ \to X + (- \frac{1}{6}) = X - (\frac{1}{6})$
98	82 90 97	3eqtrd	$⊢ X \in ℂ \to \sum_{k = 0}^{0 + 1} (\binom{2}{k}) (\frac{k BernPoly X}{2 - k + 1}) = X - (\frac{1}{6})$
99	8 98	eqtrid	$⊢ X \in ℂ \to \sum_{k = 0}^{2 - 1} (\binom{2}{k}) (\frac{k BernPoly X}{2 - k + 1}) = X - (\frac{1}{6})$
100	99	oveq2d	$⊢ X \in ℂ \to X^{2} - \sum_{k = 0}^{2 - 1} (\binom{2}{k}) (\frac{k BernPoly X}{2 - k + 1}) = X^{2} - (X - (\frac{1}{6}))$
101		sqcl	$⊢ X \in ℂ \to X^{2} \in ℂ$
102		subsub	$⊢ (X^{2} \in ℂ \land X \in ℂ \land \frac{1}{6} \in ℂ) \to X^{2} - (X - (\frac{1}{6})) = X^{2} - X + (\frac{1}{6})$
103	95 102	mp3an3	$⊢ (X^{2} \in ℂ \land X \in ℂ) \to X^{2} - (X - (\frac{1}{6})) = X^{2} - X + (\frac{1}{6})$
104	101 103	mpancom	$⊢ X \in ℂ \to X^{2} - (X - (\frac{1}{6})) = X^{2} - X + (\frac{1}{6})$
105	3 100 104	3eqtrd	$⊢ X \in ℂ \to 2 BernPoly X = X^{2} - X + (\frac{1}{6})$

Metamath Proof Explorer

Theorem bpoly2

Proof