bpoly3

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

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

Proof

Step	Hyp	Ref	Expression
1		3nn0	$⊢ 3 \in ℕ_{0}$
2		bpolyval	$⊢ (3 \in ℕ_{0} \land X \in ℂ) \to 3 BernPoly X = X^{3} - \sum_{k = 0}^{3 - 1} (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1})$
3	1 2	mpan	$⊢ X \in ℂ \to 3 BernPoly X = X^{3} - \sum_{k = 0}^{3 - 1} (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1})$
4		3m1e2	$⊢ 3 - 1 = 2$
5		df-2	$⊢ 2 = 1 + 1$
6	4 5	eqtri	$⊢ 3 - 1 = 1 + 1$
7	6	oveq2i	$⊢ (0 \dots 3 - 1) = (0 \dots 1 + 1)$
8	7	sumeq1i	$⊢ \sum_{k = 0}^{3 - 1} (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) = \sum_{k = 0}^{1 + 1} (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1})$
9		1eluzge0	$⊢ 1 \in ℤ_{\geq 0}$
10	9	a1i	$⊢ X \in ℂ \to 1 \in ℤ_{\geq 0}$
11		0z	$⊢ 0 \in ℤ$
12		fzpr	$⊢ 0 \in ℤ \to (0 \dots 0 + 1) = \{0, 0 + 1\}$
13	11 12	ax-mp	$⊢ (0 \dots 0 + 1) = \{0, 0 + 1\}$
14		0p1e1	$⊢ 0 + 1 = 1$
15	14	oveq2i	$⊢ (0 \dots 0 + 1) = (0 \dots 1)$
16	14	preq2i	$⊢ \{0, 0 + 1\} = \{0, 1\}$
17	13 15 16	3eqtr3ri	$⊢ \{0, 1\} = (0 \dots 1)$
18	5	sneqi	$⊢ \{2\} = \{1 + 1\}$
19	17 18	uneq12i	$⊢ \{0, 1\} \cup \{2\} = (0 \dots 1) \cup \{1 + 1\}$
20		df-tp	$⊢ \{0, 1, 2\} = \{0, 1\} \cup \{2\}$
21		fzsuc	$⊢ 1 \in ℤ_{\geq 0} \to (0 \dots 1 + 1) = (0 \dots 1) \cup \{1 + 1\}$
22	9 21	ax-mp	$⊢ (0 \dots 1 + 1) = (0 \dots 1) \cup \{1 + 1\}$
23	19 20 22	3eqtr4ri	$⊢ (0 \dots 1 + 1) = \{0, 1, 2\}$
24	23	eleq2i	$⊢ k \in (0 \dots 1 + 1) \leftrightarrow k \in \{0, 1, 2\}$
25		vex	$⊢ k \in V$
26	25	eltp	$⊢ k \in \{0, 1, 2\} \leftrightarrow (k = 0 \lor k = 1 \lor k = 2)$
27	24 26	bitri	$⊢ k \in (0 \dots 1 + 1) \leftrightarrow (k = 0 \lor k = 1 \lor k = 2)$
28		oveq2	$⊢ k = 0 \to (\binom{3}{k}) = (\binom{3}{0})$
29		bcn0	$⊢ 3 \in ℕ_{0} \to (\binom{3}{0}) = 1$
30	1 29	ax-mp	$⊢ (\binom{3}{0}) = 1$
31	28 30	eqtrdi	$⊢ k = 0 \to (\binom{3}{k}) = 1$
32		oveq1	$⊢ k = 0 \to k BernPoly X = 0 BernPoly X$
33		oveq2	$⊢ k = 0 \to 3 - k = 3 - 0$
34	33	oveq1d	$⊢ k = 0 \to 3 - k + 1 = 3 - 0 + 1$
35		3cn	$⊢ 3 \in ℂ$
36	35	subid1i	$⊢ 3 - 0 = 3$
37	36	oveq1i	$⊢ 3 - 0 + 1 = 3 + 1$
38		df-4	$⊢ 4 = 3 + 1$
39	37 38	eqtr4i	$⊢ 3 - 0 + 1 = 4$
40	34 39	eqtrdi	$⊢ k = 0 \to 3 - k + 1 = 4$
41	32 40	oveq12d	$⊢ k = 0 \to \frac{k BernPoly X}{3 - k + 1} = \frac{0 BernPoly X}{4}$
42	31 41	oveq12d	$⊢ k = 0 \to (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) = 1 (\frac{0 BernPoly X}{4})$
43		bpoly0	$⊢ X \in ℂ \to 0 BernPoly X = 1$
44	43	oveq1d	$⊢ X \in ℂ \to \frac{0 BernPoly X}{4} = \frac{1}{4}$
45	44	oveq2d	$⊢ X \in ℂ \to 1 (\frac{0 BernPoly X}{4}) = 1 (\frac{1}{4})$
46		4cn	$⊢ 4 \in ℂ$
47		4ne0	$⊢ 4 \neq 0$
48	46 47	reccli	$⊢ \frac{1}{4} \in ℂ$
49	48	mullidi	$⊢ 1 (\frac{1}{4}) = \frac{1}{4}$
50	45 49	eqtrdi	$⊢ X \in ℂ \to 1 (\frac{0 BernPoly X}{4}) = \frac{1}{4}$
51	42 50	sylan9eqr	$⊢ (X \in ℂ \land k = 0) \to (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) = \frac{1}{4}$
52	51 48	eqeltrdi	$⊢ (X \in ℂ \land k = 0) \to (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) \in ℂ$
53		oveq2	$⊢ k = 1 \to (\binom{3}{k}) = (\binom{3}{1})$
54		bcn1	$⊢ 3 \in ℕ_{0} \to (\binom{3}{1}) = 3$
55	1 54	ax-mp	$⊢ (\binom{3}{1}) = 3$
56	53 55	eqtrdi	$⊢ k = 1 \to (\binom{3}{k}) = 3$
57		oveq1	$⊢ k = 1 \to k BernPoly X = 1 BernPoly X$
58		oveq2	$⊢ k = 1 \to 3 - k = 3 - 1$
59	58	oveq1d	$⊢ k = 1 \to 3 - k + 1 = 3 - 1 + 1$
60		ax-1cn	$⊢ 1 \in ℂ$
61		npcan	$⊢ (3 \in ℂ \land 1 \in ℂ) \to 3 - 1 + 1 = 3$
62	35 60 61	mp2an	$⊢ 3 - 1 + 1 = 3$
63	59 62	eqtrdi	$⊢ k = 1 \to 3 - k + 1 = 3$
64	57 63	oveq12d	$⊢ k = 1 \to \frac{k BernPoly X}{3 - k + 1} = \frac{1 BernPoly X}{3}$
65	56 64	oveq12d	$⊢ k = 1 \to (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) = 3 (\frac{1 BernPoly X}{3})$
66		bpoly1	$⊢ X \in ℂ \to 1 BernPoly X = X - (\frac{1}{2})$
67	66	oveq1d	$⊢ X \in ℂ \to \frac{1 BernPoly X}{3} = \frac{X - (\frac{1}{2})}{3}$
68	67	oveq2d	$⊢ X \in ℂ \to 3 (\frac{1 BernPoly X}{3}) = 3 (\frac{X - (\frac{1}{2})}{3})$
69		halfcn	$⊢ \frac{1}{2} \in ℂ$
70		subcl	$⊢ (X \in ℂ \land \frac{1}{2} \in ℂ) \to X - (\frac{1}{2}) \in ℂ$
71	69 70	mpan2	$⊢ X \in ℂ \to X - (\frac{1}{2}) \in ℂ$
72		3ne0	$⊢ 3 \neq 0$
73		divcan2	$⊢ (X - (\frac{1}{2}) \in ℂ \land 3 \in ℂ \land 3 \neq 0) \to 3 (\frac{X - (\frac{1}{2})}{3}) = X - (\frac{1}{2})$
74	35 72 73	mp3an23	$⊢ X - (\frac{1}{2}) \in ℂ \to 3 (\frac{X - (\frac{1}{2})}{3}) = X - (\frac{1}{2})$
75	71 74	syl	$⊢ X \in ℂ \to 3 (\frac{X - (\frac{1}{2})}{3}) = X - (\frac{1}{2})$
76	68 75	eqtrd	$⊢ X \in ℂ \to 3 (\frac{1 BernPoly X}{3}) = X - (\frac{1}{2})$
77	65 76	sylan9eqr	$⊢ (X \in ℂ \land k = 1) \to (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) = X - (\frac{1}{2})$
78	71	adantr	$⊢ (X \in ℂ \land k = 1) \to X - (\frac{1}{2}) \in ℂ$
79	77 78	eqeltrd	$⊢ (X \in ℂ \land k = 1) \to (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) \in ℂ$
80		oveq2	$⊢ k = 2 \to (\binom{3}{k}) = (\binom{3}{2})$
81		bcn2	$⊢ 3 \in ℕ_{0} \to (\binom{3}{2}) = \frac{3 (3 - 1)}{2}$
82	1 81	ax-mp	$⊢ (\binom{3}{2}) = \frac{3 (3 - 1)}{2}$
83	4	oveq2i	$⊢ 3 (3 - 1) = 3 \cdot 2$
84	83	oveq1i	$⊢ \frac{3 (3 - 1)}{2} = \frac{3 \cdot 2}{2}$
85		2cn	$⊢ 2 \in ℂ$
86		2ne0	$⊢ 2 \neq 0$
87	35 85 86	divcan4i	$⊢ \frac{3 \cdot 2}{2} = 3$
88	84 87	eqtri	$⊢ \frac{3 (3 - 1)}{2} = 3$
89	82 88	eqtri	$⊢ (\binom{3}{2}) = 3$
90	80 89	eqtrdi	$⊢ k = 2 \to (\binom{3}{k}) = 3$
91		oveq1	$⊢ k = 2 \to k BernPoly X = 2 BernPoly X$
92		oveq2	$⊢ k = 2 \to 3 - k = 3 - 2$
93	92	oveq1d	$⊢ k = 2 \to 3 - k + 1 = 3 - 2 + 1$
94		2p1e3	$⊢ 2 + 1 = 3$
95	35 85 60 94	subaddrii	$⊢ 3 - 2 = 1$
96	95	oveq1i	$⊢ 3 - 2 + 1 = 1 + 1$
97	96 5	eqtr4i	$⊢ 3 - 2 + 1 = 2$
98	93 97	eqtrdi	$⊢ k = 2 \to 3 - k + 1 = 2$
99	91 98	oveq12d	$⊢ k = 2 \to \frac{k BernPoly X}{3 - k + 1} = \frac{2 BernPoly X}{2}$
100	90 99	oveq12d	$⊢ k = 2 \to (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) = 3 (\frac{2 BernPoly X}{2})$
101		2nn0	$⊢ 2 \in ℕ_{0}$
102		bpolycl	$⊢ (2 \in ℕ_{0} \land X \in ℂ) \to 2 BernPoly X \in ℂ$
103	101 102	mpan	$⊢ X \in ℂ \to 2 BernPoly X \in ℂ$
104		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
105		div12	$⊢ (3 \in ℂ \land 2 BernPoly X \in ℂ \land (2 \in ℂ \land 2 \neq 0)) \to 3 (\frac{2 BernPoly X}{2}) = (2 BernPoly X) (\frac{3}{2})$
106	35 104 105	mp3an13	$⊢ 2 BernPoly X \in ℂ \to 3 (\frac{2 BernPoly X}{2}) = (2 BernPoly X) (\frac{3}{2})$
107	103 106	syl	$⊢ X \in ℂ \to 3 (\frac{2 BernPoly X}{2}) = (2 BernPoly X) (\frac{3}{2})$
108	35 85 86	divcli	$⊢ \frac{3}{2} \in ℂ$
109		mulcom	$⊢ (2 BernPoly X \in ℂ \land \frac{3}{2} \in ℂ) \to (2 BernPoly X) (\frac{3}{2}) = (\frac{3}{2}) (2 BernPoly X)$
110	103 108 109	sylancl	$⊢ X \in ℂ \to (2 BernPoly X) (\frac{3}{2}) = (\frac{3}{2}) (2 BernPoly X)$
111		bpoly2	$⊢ X \in ℂ \to 2 BernPoly X = X^{2} - X + (\frac{1}{6})$
112	111	oveq2d	$⊢ X \in ℂ \to (\frac{3}{2}) (2 BernPoly X) = (\frac{3}{2}) (X^{2} - X + (\frac{1}{6}))$
113		sqcl	$⊢ X \in ℂ \to X^{2} \in ℂ$
114		6cn	$⊢ 6 \in ℂ$
115		6re	$⊢ 6 \in ℝ$
116		6pos	$⊢ 0 < 6$
117	115 116	gt0ne0ii	$⊢ 6 \neq 0$
118	114 117	reccli	$⊢ \frac{1}{6} \in ℂ$
119		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})$
120	118 119	mp3an3	$⊢ (X^{2} \in ℂ \land X \in ℂ) \to X^{2} - (X - (\frac{1}{6})) = X^{2} - X + (\frac{1}{6})$
121	113 120	mpancom	$⊢ X \in ℂ \to X^{2} - (X - (\frac{1}{6})) = X^{2} - X + (\frac{1}{6})$
122	121	oveq2d	$⊢ X \in ℂ \to (\frac{3}{2}) (X^{2} - (X - (\frac{1}{6}))) = (\frac{3}{2}) (X^{2} - X + (\frac{1}{6}))$
123		subcl	$⊢ (X \in ℂ \land \frac{1}{6} \in ℂ) \to X - (\frac{1}{6}) \in ℂ$
124	118 123	mpan2	$⊢ X \in ℂ \to X - (\frac{1}{6}) \in ℂ$
125		subdi	$⊢ (\frac{3}{2} \in ℂ \land X^{2} \in ℂ \land X - (\frac{1}{6}) \in ℂ) \to (\frac{3}{2}) (X^{2} - (X - (\frac{1}{6}))) = (\frac{3}{2}) X^{2} - (\frac{3}{2}) (X - (\frac{1}{6}))$
126	108 113 124 125	mp3an2i	$⊢ X \in ℂ \to (\frac{3}{2}) (X^{2} - (X - (\frac{1}{6}))) = (\frac{3}{2}) X^{2} - (\frac{3}{2}) (X - (\frac{1}{6}))$
127	112 122 126	3eqtr2d	$⊢ X \in ℂ \to (\frac{3}{2}) (2 BernPoly X) = (\frac{3}{2}) X^{2} - (\frac{3}{2}) (X - (\frac{1}{6}))$
128	107 110 127	3eqtrd	$⊢ X \in ℂ \to 3 (\frac{2 BernPoly X}{2}) = (\frac{3}{2}) X^{2} - (\frac{3}{2}) (X - (\frac{1}{6}))$
129	100 128	sylan9eqr	$⊢ (X \in ℂ \land k = 2) \to (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) = (\frac{3}{2}) X^{2} - (\frac{3}{2}) (X - (\frac{1}{6}))$
130		mulcl	$⊢ (\frac{3}{2} \in ℂ \land X^{2} \in ℂ) \to (\frac{3}{2}) X^{2} \in ℂ$
131	108 113 130	sylancr	$⊢ X \in ℂ \to (\frac{3}{2}) X^{2} \in ℂ$
132		mulcl	$⊢ (\frac{3}{2} \in ℂ \land X - (\frac{1}{6}) \in ℂ) \to (\frac{3}{2}) (X - (\frac{1}{6})) \in ℂ$
133	108 124 132	sylancr	$⊢ X \in ℂ \to (\frac{3}{2}) (X - (\frac{1}{6})) \in ℂ$
134	131 133	subcld	$⊢ X \in ℂ \to (\frac{3}{2}) X^{2} - (\frac{3}{2}) (X - (\frac{1}{6})) \in ℂ$
135	134	adantr	$⊢ (X \in ℂ \land k = 2) \to (\frac{3}{2}) X^{2} - (\frac{3}{2}) (X - (\frac{1}{6})) \in ℂ$
136	129 135	eqeltrd	$⊢ (X \in ℂ \land k = 2) \to (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) \in ℂ$
137	52 79 136	3jaodan	$⊢ (X \in ℂ \land (k = 0 \lor k = 1 \lor k = 2)) \to (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) \in ℂ$
138	27 137	sylan2b	$⊢ (X \in ℂ \land k \in (0 \dots 1 + 1)) \to (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) \in ℂ$
139	5	eqeq2i	$⊢ k = 2 \leftrightarrow k = 1 + 1$
140	139 100	sylbir	$⊢ k = 1 + 1 \to (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) = 3 (\frac{2 BernPoly X}{2})$
141	10 138 140	fsump1	$⊢ X \in ℂ \to \sum_{k = 0}^{1 + 1} (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) = \sum_{k = 0}^{1} (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) + 3 (\frac{2 BernPoly X}{2})$
142	128	oveq2d	$⊢ X \in ℂ \to \sum_{k = 0}^{1} (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) + 3 (\frac{2 BernPoly X}{2}) = \sum_{k = 0}^{1} (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) + (\frac{3}{2}) X^{2} - (\frac{3}{2}) (X - (\frac{1}{6}))$
143	15	sumeq1i	$⊢ \sum_{k = 0}^{0 + 1} (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) = \sum_{k = 0}^{1} (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1})$
144		0nn0	$⊢ 0 \in ℕ_{0}$
145		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
146	144 145	eleqtri	$⊢ 0 \in ℤ_{\geq 0}$
147	146	a1i	$⊢ X \in ℂ \to 0 \in ℤ_{\geq 0}$
148	13 16	eqtri	$⊢ (0 \dots 0 + 1) = \{0, 1\}$
149	148	eleq2i	$⊢ k \in (0 \dots 0 + 1) \leftrightarrow k \in \{0, 1\}$
150	25	elpr	$⊢ k \in \{0, 1\} \leftrightarrow (k = 0 \lor k = 1)$
151	149 150	bitri	$⊢ k \in (0 \dots 0 + 1) \leftrightarrow (k = 0 \lor k = 1)$
152	52 79	jaodan	$⊢ (X \in ℂ \land (k = 0 \lor k = 1)) \to (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) \in ℂ$
153	151 152	sylan2b	$⊢ (X \in ℂ \land k \in (0 \dots 0 + 1)) \to (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) \in ℂ$
154	14	eqeq2i	$⊢ k = 0 + 1 \leftrightarrow k = 1$
155	154 65	sylbi	$⊢ k = 0 + 1 \to (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) = 3 (\frac{1 BernPoly X}{3})$
156	147 153 155	fsump1	$⊢ X \in ℂ \to \sum_{k = 0}^{0 + 1} (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) = \sum_{k = 0}^{0} (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) + 3 (\frac{1 BernPoly X}{3})$
157	50 48	eqeltrdi	$⊢ X \in ℂ \to 1 (\frac{0 BernPoly X}{4}) \in ℂ$
158	42	fsum1	$⊢ (0 \in ℤ \land 1 (\frac{0 BernPoly X}{4}) \in ℂ) \to \sum_{k = 0}^{0} (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) = 1 (\frac{0 BernPoly X}{4})$
159	11 157 158	sylancr	$⊢ X \in ℂ \to \sum_{k = 0}^{0} (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) = 1 (\frac{0 BernPoly X}{4})$
160	159 50	eqtrd	$⊢ X \in ℂ \to \sum_{k = 0}^{0} (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) = \frac{1}{4}$
161	160 76	oveq12d	$⊢ X \in ℂ \to \sum_{k = 0}^{0} (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) + 3 (\frac{1 BernPoly X}{3}) = (\frac{1}{4}) + X - (\frac{1}{2})$
162	156 161	eqtrd	$⊢ X \in ℂ \to \sum_{k = 0}^{0 + 1} (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) = (\frac{1}{4}) + X - (\frac{1}{2})$
163	143 162	eqtr3id	$⊢ X \in ℂ \to \sum_{k = 0}^{1} (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) = (\frac{1}{4}) + X - (\frac{1}{2})$
164	163	oveq1d	$⊢ X \in ℂ \to \sum_{k = 0}^{1} (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) + (\frac{3}{2}) X^{2} - (\frac{3}{2}) (X - (\frac{1}{6})) = (\frac{1}{4}) + (X - (\frac{1}{2})) + ((\frac{3}{2}) X^{2} - (\frac{3}{2}) (X - (\frac{1}{6})))$
165		addcl	$⊢ (\frac{1}{4} \in ℂ \land X - (\frac{1}{2}) \in ℂ) \to (\frac{1}{4}) + X - (\frac{1}{2}) \in ℂ$
166	48 71 165	sylancr	$⊢ X \in ℂ \to (\frac{1}{4}) + X - (\frac{1}{2}) \in ℂ$
167	166 131 133	addsub12d	$⊢ X \in ℂ \to (\frac{1}{4}) + (X - (\frac{1}{2})) + ((\frac{3}{2}) X^{2} - (\frac{3}{2}) (X - (\frac{1}{6}))) = (\frac{3}{2}) X^{2} + ((\frac{1}{4}) + X - (\frac{1}{2})) - (\frac{3}{2}) (X - (\frac{1}{6}))$
168	164 167	eqtrd	$⊢ X \in ℂ \to \sum_{k = 0}^{1} (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) + (\frac{3}{2}) X^{2} - (\frac{3}{2}) (X - (\frac{1}{6})) = (\frac{3}{2}) X^{2} + ((\frac{1}{4}) + X - (\frac{1}{2})) - (\frac{3}{2}) (X - (\frac{1}{6}))$
169	133 166	negsubdi2d	$⊢ X \in ℂ \to - ((\frac{3}{2}) (X - (\frac{1}{6})) - ((\frac{1}{4}) + X - (\frac{1}{2}))) = (\frac{1}{4}) + (X - (\frac{1}{2})) - (\frac{3}{2}) (X - (\frac{1}{6}))$
170		subdi	$⊢ (\frac{3}{2} \in ℂ \land X \in ℂ \land \frac{1}{6} \in ℂ) \to (\frac{3}{2}) (X - (\frac{1}{6})) = (\frac{3}{2}) X - (\frac{3}{2}) (\frac{1}{6})$
171	108 118 170	mp3an13	$⊢ X \in ℂ \to (\frac{3}{2}) (X - (\frac{1}{6})) = (\frac{3}{2}) X - (\frac{3}{2}) (\frac{1}{6})$
172		addsub12	$⊢ (\frac{1}{4} \in ℂ \land X \in ℂ \land \frac{1}{2} \in ℂ) \to (\frac{1}{4}) + X - (\frac{1}{2}) = X + (\frac{1}{4}) - (\frac{1}{2})$
173	48 69 172	mp3an13	$⊢ X \in ℂ \to (\frac{1}{4}) + X - (\frac{1}{2}) = X + (\frac{1}{4}) - (\frac{1}{2})$
174	171 173	oveq12d	$⊢ X \in ℂ \to (\frac{3}{2}) (X - (\frac{1}{6})) - ((\frac{1}{4}) + X - (\frac{1}{2})) = (\frac{3}{2}) X - (\frac{3}{2}) (\frac{1}{6}) - (X + (\frac{1}{4}) - (\frac{1}{2}))$
175		mulcl	$⊢ (\frac{3}{2} \in ℂ \land X \in ℂ) \to (\frac{3}{2}) X \in ℂ$
176	108 175	mpan	$⊢ X \in ℂ \to (\frac{3}{2}) X \in ℂ$
177	108 118	mulcli	$⊢ (\frac{3}{2}) (\frac{1}{6}) \in ℂ$
178		negsub	$⊢ ((\frac{3}{2}) X \in ℂ \land (\frac{3}{2}) (\frac{1}{6}) \in ℂ) \to (\frac{3}{2}) X + (- (\frac{3}{2}) (\frac{1}{6})) = (\frac{3}{2}) X - (\frac{3}{2}) (\frac{1}{6})$
179	176 177 178	sylancl	$⊢ X \in ℂ \to (\frac{3}{2}) X + (- (\frac{3}{2}) (\frac{1}{6})) = (\frac{3}{2}) X - (\frac{3}{2}) (\frac{1}{6})$
180	179	oveq1d	$⊢ X \in ℂ \to (\frac{3}{2}) X + (- (\frac{3}{2}) (\frac{1}{6})) - (X + (\frac{1}{4}) - (\frac{1}{2})) = (\frac{3}{2}) X - (\frac{3}{2}) (\frac{1}{6}) - (X + (\frac{1}{4}) - (\frac{1}{2}))$
181	69 48	negsubdi2i	$⊢ - ((\frac{1}{2}) - (\frac{1}{4})) = (\frac{1}{4}) - (\frac{1}{2})$
182	85 35 85	mul12i	$⊢ 2 3 \cdot 2 = 3 2 \cdot 2$
183		3t2e6	$⊢ 3 \cdot 2 = 6$
184	183	oveq2i	$⊢ 2 3 \cdot 2 = 2 \cdot 6$
185		2t2e4	$⊢ 2 \cdot 2 = 4$
186	185	oveq2i	$⊢ 3 2 \cdot 2 = 3 \cdot 4$
187	182 184 186	3eqtr3i	$⊢ 2 \cdot 6 = 3 \cdot 4$
188	187	oveq2i	$⊢ \frac{3 \cdot 1}{2 \cdot 6} = \frac{3 \cdot 1}{3 \cdot 4}$
189	46 47	pm3.2i	$⊢ (4 \in ℂ \land 4 \neq 0)$
190	35 72	pm3.2i	$⊢ (3 \in ℂ \land 3 \neq 0)$
191		divcan5	$⊢ (1 \in ℂ \land (4 \in ℂ \land 4 \neq 0) \land (3 \in ℂ \land 3 \neq 0)) \to \frac{3 \cdot 1}{3 \cdot 4} = \frac{1}{4}$
192	60 189 190 191	mp3an	$⊢ \frac{3 \cdot 1}{3 \cdot 4} = \frac{1}{4}$
193	188 192	eqtri	$⊢ \frac{3 \cdot 1}{2 \cdot 6} = \frac{1}{4}$
194	35 85 60 114 86 117	divmuldivi	$⊢ (\frac{3}{2}) (\frac{1}{6}) = \frac{3 \cdot 1}{2 \cdot 6}$
195		2t1e2	$⊢ 2 \cdot 1 = 2$
196	195 5	eqtri	$⊢ 2 \cdot 1 = 1 + 1$
197	196 185	oveq12i	$⊢ \frac{2 \cdot 1}{2 \cdot 2} = \frac{1 + 1}{4}$
198		divcan5	$⊢ (1 \in ℂ \land (2 \in ℂ \land 2 \neq 0) \land (2 \in ℂ \land 2 \neq 0)) \to \frac{2 \cdot 1}{2 \cdot 2} = \frac{1}{2}$
199	60 104 104 198	mp3an	$⊢ \frac{2 \cdot 1}{2 \cdot 2} = \frac{1}{2}$
200	60 60 46 47	divdiri	$⊢ \frac{1 + 1}{4} = (\frac{1}{4}) + (\frac{1}{4})$
201	197 199 200	3eqtr3ri	$⊢ (\frac{1}{4}) + (\frac{1}{4}) = \frac{1}{2}$
202	69 48 48 201	subaddrii	$⊢ (\frac{1}{2}) - (\frac{1}{4}) = \frac{1}{4}$
203	193 194 202	3eqtr4ri	$⊢ (\frac{1}{2}) - (\frac{1}{4}) = (\frac{3}{2}) (\frac{1}{6})$
204	203	negeqi	$⊢ - ((\frac{1}{2}) - (\frac{1}{4})) = - (\frac{3}{2}) (\frac{1}{6})$
205	181 204	eqtr3i	$⊢ (\frac{1}{4}) - (\frac{1}{2}) = - (\frac{3}{2}) (\frac{1}{6})$
206	48 69	subcli	$⊢ (\frac{1}{4}) - (\frac{1}{2}) \in ℂ$
207	177	negcli	$⊢ - (\frac{3}{2}) (\frac{1}{6}) \in ℂ$
208	206 207	subeq0i	$⊢ (\frac{1}{4}) - (\frac{1}{2}) - (- (\frac{3}{2}) (\frac{1}{6})) = 0 \leftrightarrow (\frac{1}{4}) - (\frac{1}{2}) = - (\frac{3}{2}) (\frac{1}{6})$
209	205 208	mpbir	$⊢ (\frac{1}{4}) - (\frac{1}{2}) - (- (\frac{3}{2}) (\frac{1}{6})) = 0$
210	209	oveq2i	$⊢ (\frac{3}{2}) X - X - ((\frac{1}{4}) - (\frac{1}{2}) - (- (\frac{3}{2}) (\frac{1}{6}))) = (\frac{3}{2}) X - X - 0$
211		id	$⊢ X \in ℂ \to X \in ℂ$
212	206	a1i	$⊢ X \in ℂ \to (\frac{1}{4}) - (\frac{1}{2}) \in ℂ$
213	207	a1i	$⊢ X \in ℂ \to - (\frac{3}{2}) (\frac{1}{6}) \in ℂ$
214	176 211 212 213	subadd4d	$⊢ X \in ℂ \to (\frac{3}{2}) X - X - ((\frac{1}{4}) - (\frac{1}{2}) - (- (\frac{3}{2}) (\frac{1}{6}))) = (\frac{3}{2}) X + (- (\frac{3}{2}) (\frac{1}{6})) - (X + (\frac{1}{4}) - (\frac{1}{2}))$
215		subdir	$⊢ (\frac{3}{2} \in ℂ \land 1 \in ℂ \land X \in ℂ) \to ((\frac{3}{2}) - 1) X = (\frac{3}{2}) X - 1 X$
216	108 60 215	mp3an12	$⊢ X \in ℂ \to ((\frac{3}{2}) - 1) X = (\frac{3}{2}) X - 1 X$
217		divsubdir	$⊢ (3 \in ℂ \land 2 \in ℂ \land (2 \in ℂ \land 2 \neq 0)) \to \frac{3 - 2}{2} = (\frac{3}{2}) - (\frac{2}{2})$
218	35 85 104 217	mp3an	$⊢ \frac{3 - 2}{2} = (\frac{3}{2}) - (\frac{2}{2})$
219	95	oveq1i	$⊢ \frac{3 - 2}{2} = \frac{1}{2}$
220		2div2e1	$⊢ \frac{2}{2} = 1$
221	220	oveq2i	$⊢ (\frac{3}{2}) - (\frac{2}{2}) = (\frac{3}{2}) - 1$
222	218 219 221	3eqtr3ri	$⊢ (\frac{3}{2}) - 1 = \frac{1}{2}$
223	222	oveq1i	$⊢ ((\frac{3}{2}) - 1) X = (\frac{1}{2}) X$
224	223	a1i	$⊢ X \in ℂ \to ((\frac{3}{2}) - 1) X = (\frac{1}{2}) X$
225		mullid	$⊢ X \in ℂ \to 1 X = X$
226	225	oveq2d	$⊢ X \in ℂ \to (\frac{3}{2}) X - 1 X = (\frac{3}{2}) X - X$
227	216 224 226	3eqtr3rd	$⊢ X \in ℂ \to (\frac{3}{2}) X - X = (\frac{1}{2}) X$
228	227	oveq1d	$⊢ X \in ℂ \to (\frac{3}{2}) X - X - 0 = (\frac{1}{2}) X - 0$
229		mulcl	$⊢ (\frac{1}{2} \in ℂ \land X \in ℂ) \to (\frac{1}{2}) X \in ℂ$
230	69 229	mpan	$⊢ X \in ℂ \to (\frac{1}{2}) X \in ℂ$
231	230	subid1d	$⊢ X \in ℂ \to (\frac{1}{2}) X - 0 = (\frac{1}{2}) X$
232	228 231	eqtrd	$⊢ X \in ℂ \to (\frac{3}{2}) X - X - 0 = (\frac{1}{2}) X$
233	210 214 232	3eqtr3a	$⊢ X \in ℂ \to (\frac{3}{2}) X + (- (\frac{3}{2}) (\frac{1}{6})) - (X + (\frac{1}{4}) - (\frac{1}{2})) = (\frac{1}{2}) X$
234	174 180 233	3eqtr2d	$⊢ X \in ℂ \to (\frac{3}{2}) (X - (\frac{1}{6})) - ((\frac{1}{4}) + X - (\frac{1}{2})) = (\frac{1}{2}) X$
235	234	negeqd	$⊢ X \in ℂ \to - ((\frac{3}{2}) (X - (\frac{1}{6})) - ((\frac{1}{4}) + X - (\frac{1}{2}))) = - (\frac{1}{2}) X$
236	169 235	eqtr3d	$⊢ X \in ℂ \to (\frac{1}{4}) + (X - (\frac{1}{2})) - (\frac{3}{2}) (X - (\frac{1}{6})) = - (\frac{1}{2}) X$
237	236	oveq2d	$⊢ X \in ℂ \to (\frac{3}{2}) X^{2} + ((\frac{1}{4}) + X - (\frac{1}{2})) - (\frac{3}{2}) (X - (\frac{1}{6})) = (\frac{3}{2}) X^{2} + (- (\frac{1}{2}) X)$
238	131 230	negsubd	$⊢ X \in ℂ \to (\frac{3}{2}) X^{2} + (- (\frac{1}{2}) X) = (\frac{3}{2}) X^{2} - (\frac{1}{2}) X$
239	168 237 238	3eqtrd	$⊢ X \in ℂ \to \sum_{k = 0}^{1} (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) + (\frac{3}{2}) X^{2} - (\frac{3}{2}) (X - (\frac{1}{6})) = (\frac{3}{2}) X^{2} - (\frac{1}{2}) X$
240	141 142 239	3eqtrd	$⊢ X \in ℂ \to \sum_{k = 0}^{1 + 1} (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) = (\frac{3}{2}) X^{2} - (\frac{1}{2}) X$
241	8 240	eqtrid	$⊢ X \in ℂ \to \sum_{k = 0}^{3 - 1} (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) = (\frac{3}{2}) X^{2} - (\frac{1}{2}) X$
242	241	oveq2d	$⊢ X \in ℂ \to X^{3} - \sum_{k = 0}^{3 - 1} (\binom{3}{k}) (\frac{k BernPoly X}{3 - k + 1}) = X^{3} - ((\frac{3}{2}) X^{2} - (\frac{1}{2}) X)$
243		expcl	$⊢ (X \in ℂ \land 3 \in ℕ_{0}) \to X^{3} \in ℂ$
244	1 243	mpan2	$⊢ X \in ℂ \to X^{3} \in ℂ$
245	244 131 230	subsubd	$⊢ X \in ℂ \to X^{3} - ((\frac{3}{2}) X^{2} - (\frac{1}{2}) X) = X^{3} - (\frac{3}{2}) X^{2} + (\frac{1}{2}) X$
246	3 242 245	3eqtrd	$⊢ X \in ℂ \to 3 BernPoly X = X^{3} - (\frac{3}{2}) X^{2} + (\frac{1}{2}) X$

Metamath Proof Explorer

Theorem bpoly3

Proof