bpoly4

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

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

Proof

Step	Hyp	Ref	Expression
1		4nn0	$⊢ 4 \in ℕ_{0}$
2		bpolyval	$⊢ (4 \in ℕ_{0} \land X \in ℂ) \to 4 BernPoly X = X^{4} - \sum_{k = 0}^{4 - 1} (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1})$
3	1 2	mpan	$⊢ X \in ℂ \to 4 BernPoly X = X^{4} - \sum_{k = 0}^{4 - 1} (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1})$
4		4m1e3	$⊢ 4 - 1 = 3$
5		df-3	$⊢ 3 = 2 + 1$
6	4 5	eqtri	$⊢ 4 - 1 = 2 + 1$
7	6	oveq2i	$⊢ (0 \dots 4 - 1) = (0 \dots 2 + 1)$
8	7	sumeq1i	$⊢ \sum_{k = 0}^{4 - 1} (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1}) = \sum_{k = 0}^{2 + 1} (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1})$
9		2eluzge0	$⊢ 2 \in ℤ_{\geq 0}$
10	9	a1i	$⊢ X \in ℂ \to 2 \in ℤ_{\geq 0}$
11		elfzelz	$⊢ k \in (0 \dots 2 + 1) \to k \in ℤ$
12		bccl	$⊢ (4 \in ℕ_{0} \land k \in ℤ) \to (\binom{4}{k}) \in ℕ_{0}$
13	1 11 12	sylancr	$⊢ k \in (0 \dots 2 + 1) \to (\binom{4}{k}) \in ℕ_{0}$
14	13	nn0cnd	$⊢ k \in (0 \dots 2 + 1) \to (\binom{4}{k}) \in ℂ$
15	14	adantl	$⊢ (X \in ℂ \land k \in (0 \dots 2 + 1)) \to (\binom{4}{k}) \in ℂ$
16		elfznn0	$⊢ k \in (0 \dots 2 + 1) \to k \in ℕ_{0}$
17		bpolycl	$⊢ (k \in ℕ_{0} \land X \in ℂ) \to k BernPoly X \in ℂ$
18	16 17	sylan	$⊢ (k \in (0 \dots 2 + 1) \land X \in ℂ) \to k BernPoly X \in ℂ$
19	18	ancoms	$⊢ (X \in ℂ \land k \in (0 \dots 2 + 1)) \to k BernPoly X \in ℂ$
20		4re	$⊢ 4 \in ℝ$
21	20	a1i	$⊢ k \in (0 \dots 2 + 1) \to 4 \in ℝ$
22	11	zred	$⊢ k \in (0 \dots 2 + 1) \to k \in ℝ$
23	21 22	resubcld	$⊢ k \in (0 \dots 2 + 1) \to 4 - k \in ℝ$
24		peano2re	$⊢ 4 - k \in ℝ \to 4 - k + 1 \in ℝ$
25	23 24	syl	$⊢ k \in (0 \dots 2 + 1) \to 4 - k + 1 \in ℝ$
26	25	recnd	$⊢ k \in (0 \dots 2 + 1) \to 4 - k + 1 \in ℂ$
27	26	adantl	$⊢ (X \in ℂ \land k \in (0 \dots 2 + 1)) \to 4 - k + 1 \in ℂ$
28		1red	$⊢ k \in (0 \dots 2 + 1) \to 1 \in ℝ$
29	5	oveq2i	$⊢ (0 \dots 3) = (0 \dots 2 + 1)$
30	29	eleq2i	$⊢ k \in (0 \dots 3) \leftrightarrow k \in (0 \dots 2 + 1)$
31		elfzelz	$⊢ k \in (0 \dots 3) \to k \in ℤ$
32	31	zred	$⊢ k \in (0 \dots 3) \to k \in ℝ$
33		3re	$⊢ 3 \in ℝ$
34	33	a1i	$⊢ k \in (0 \dots 3) \to 3 \in ℝ$
35	20	a1i	$⊢ k \in (0 \dots 3) \to 4 \in ℝ$
36		elfzle2	$⊢ k \in (0 \dots 3) \to k \leq 3$
37		3lt4	$⊢ 3 < 4$
38	37	a1i	$⊢ k \in (0 \dots 3) \to 3 < 4$
39	32 34 35 36 38	lelttrd	$⊢ k \in (0 \dots 3) \to k < 4$
40	30 39	sylbir	$⊢ k \in (0 \dots 2 + 1) \to k < 4$
41	22 21	posdifd	$⊢ k \in (0 \dots 2 + 1) \to (k < 4 \leftrightarrow 0 < 4 - k)$
42	40 41	mpbid	$⊢ k \in (0 \dots 2 + 1) \to 0 < 4 - k$
43		0lt1	$⊢ 0 < 1$
44	43	a1i	$⊢ k \in (0 \dots 2 + 1) \to 0 < 1$
45	23 28 42 44	addgt0d	$⊢ k \in (0 \dots 2 + 1) \to 0 < 4 - k + 1$
46	45	gt0ne0d	$⊢ k \in (0 \dots 2 + 1) \to 4 - k + 1 \neq 0$
47	46	adantl	$⊢ (X \in ℂ \land k \in (0 \dots 2 + 1)) \to 4 - k + 1 \neq 0$
48	19 27 47	divcld	$⊢ (X \in ℂ \land k \in (0 \dots 2 + 1)) \to \frac{k BernPoly X}{4 - k + 1} \in ℂ$
49	15 48	mulcld	$⊢ (X \in ℂ \land k \in (0 \dots 2 + 1)) \to (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1}) \in ℂ$
50	5	eqeq2i	$⊢ k = 3 \leftrightarrow k = 2 + 1$
51		oveq2	$⊢ k = 3 \to (\binom{4}{k}) = (\binom{4}{3})$
52		4bc3eq4	$⊢ (\binom{4}{3}) = 4$
53	51 52	syl6eq	$⊢ k = 3 \to (\binom{4}{k}) = 4$
54		oveq1	$⊢ k = 3 \to k BernPoly X = 3 BernPoly X$
55		oveq2	$⊢ k = 3 \to 4 - k = 4 - 3$
56	55	oveq1d	$⊢ k = 3 \to 4 - k + 1 = 4 - 3 + 1$
57		4cn	$⊢ 4 \in ℂ$
58		3cn	$⊢ 3 \in ℂ$
59		ax-1cn	$⊢ 1 \in ℂ$
60		3p1e4	$⊢ 3 + 1 = 4$
61	57 58 59 60	subaddrii	$⊢ 4 - 3 = 1$
62	61	oveq1i	$⊢ 4 - 3 + 1 = 1 + 1$
63		df-2	$⊢ 2 = 1 + 1$
64	62 63	eqtr4i	$⊢ 4 - 3 + 1 = 2$
65	56 64	syl6eq	$⊢ k = 3 \to 4 - k + 1 = 2$
66	54 65	oveq12d	$⊢ k = 3 \to \frac{k BernPoly X}{4 - k + 1} = \frac{3 BernPoly X}{2}$
67	53 66	oveq12d	$⊢ k = 3 \to (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1}) = 4 (\frac{3 BernPoly X}{2})$
68	50 67	sylbir	$⊢ k = 2 + 1 \to (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1}) = 4 (\frac{3 BernPoly X}{2})$
69	10 49 68	fsump1	$⊢ X \in ℂ \to \sum_{k = 0}^{2 + 1} (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1}) = \sum_{k = 0}^{2} (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1}) + 4 (\frac{3 BernPoly X}{2})$
70	63	oveq2i	$⊢ (0 \dots 2) = (0 \dots 1 + 1)$
71	70	sumeq1i	$⊢ \sum_{k = 0}^{2} (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1}) = \sum_{k = 0}^{1 + 1} (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1})$
72		1eluzge0	$⊢ 1 \in ℤ_{\geq 0}$
73	72	a1i	$⊢ X \in ℂ \to 1 \in ℤ_{\geq 0}$
74		fzssp1	$⊢ (0 \dots 1 + 1) \subseteq (0 \dots 1 + 1 + 1)$
75	63	oveq1i	$⊢ 2 + 1 = 1 + 1 + 1$
76	75	oveq2i	$⊢ (0 \dots 2 + 1) = (0 \dots 1 + 1 + 1)$
77	74 76	sseqtrri	$⊢ (0 \dots 1 + 1) \subseteq (0 \dots 2 + 1)$
78	77	sseli	$⊢ k \in (0 \dots 1 + 1) \to k \in (0 \dots 2 + 1)$
79	78 49	sylan2	$⊢ (X \in ℂ \land k \in (0 \dots 1 + 1)) \to (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1}) \in ℂ$
80	63	eqeq2i	$⊢ k = 2 \leftrightarrow k = 1 + 1$
81		oveq2	$⊢ k = 2 \to (\binom{4}{k}) = (\binom{4}{2})$
82		4bc2eq6	$⊢ (\binom{4}{2}) = 6$
83	81 82	syl6eq	$⊢ k = 2 \to (\binom{4}{k}) = 6$
84		oveq1	$⊢ k = 2 \to k BernPoly X = 2 BernPoly X$
85		oveq2	$⊢ k = 2 \to 4 - k = 4 - 2$
86	85	oveq1d	$⊢ k = 2 \to 4 - k + 1 = 4 - 2 + 1$
87		2cn	$⊢ 2 \in ℂ$
88		2p2e4	$⊢ 2 + 2 = 4$
89	57 87 87 88	subaddrii	$⊢ 4 - 2 = 2$
90	89	oveq1i	$⊢ 4 - 2 + 1 = 2 + 1$
91	90 5	eqtr4i	$⊢ 4 - 2 + 1 = 3$
92	86 91	syl6eq	$⊢ k = 2 \to 4 - k + 1 = 3$
93	84 92	oveq12d	$⊢ k = 2 \to \frac{k BernPoly X}{4 - k + 1} = \frac{2 BernPoly X}{3}$
94	83 93	oveq12d	$⊢ k = 2 \to (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1}) = 6 (\frac{2 BernPoly X}{3})$
95	80 94	sylbir	$⊢ k = 1 + 1 \to (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1}) = 6 (\frac{2 BernPoly X}{3})$
96	73 79 95	fsump1	$⊢ X \in ℂ \to \sum_{k = 0}^{1 + 1} (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1}) = \sum_{k = 0}^{1} (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1}) + 6 (\frac{2 BernPoly X}{3})$
97		0p1e1	$⊢ 0 + 1 = 1$
98	97	oveq2i	$⊢ (0 \dots 0 + 1) = (0 \dots 1)$
99	98	sumeq1i	$⊢ \sum_{k = 0}^{0 + 1} (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1}) = \sum_{k = 0}^{1} (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1})$
100		0nn0	$⊢ 0 \in ℕ_{0}$
101		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
102	100 101	eleqtri	$⊢ 0 \in ℤ_{\geq 0}$
103	102	a1i	$⊢ X \in ℂ \to 0 \in ℤ_{\geq 0}$
104		3nn	$⊢ 3 \in ℕ$
105		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
106	104 105	eleqtri	$⊢ 3 \in ℤ_{\geq 1}$
107		fzss2	$⊢ 3 \in ℤ_{\geq 1} \to (0 \dots 1) \subseteq (0 \dots 3)$
108	106 107	ax-mp	$⊢ (0 \dots 1) \subseteq (0 \dots 3)$
109		2p1e3	$⊢ 2 + 1 = 3$
110	109	oveq2i	$⊢ (0 \dots 2 + 1) = (0 \dots 3)$
111	108 98 110	3sstr4i	$⊢ (0 \dots 0 + 1) \subseteq (0 \dots 2 + 1)$
112	111	sseli	$⊢ k \in (0 \dots 0 + 1) \to k \in (0 \dots 2 + 1)$
113	112 49	sylan2	$⊢ (X \in ℂ \land k \in (0 \dots 0 + 1)) \to (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1}) \in ℂ$
114	97	eqeq2i	$⊢ k = 0 + 1 \leftrightarrow k = 1$
115		oveq2	$⊢ k = 1 \to (\binom{4}{k}) = (\binom{4}{1})$
116		bcn1	$⊢ 4 \in ℕ_{0} \to (\binom{4}{1}) = 4$
117	1 116	ax-mp	$⊢ (\binom{4}{1}) = 4$
118	115 117	syl6eq	$⊢ k = 1 \to (\binom{4}{k}) = 4$
119		oveq1	$⊢ k = 1 \to k BernPoly X = 1 BernPoly X$
120		oveq2	$⊢ k = 1 \to 4 - k = 4 - 1$
121	120	oveq1d	$⊢ k = 1 \to 4 - k + 1 = 4 - 1 + 1$
122	4	oveq1i	$⊢ 4 - 1 + 1 = 3 + 1$
123		df-4	$⊢ 4 = 3 + 1$
124	122 123	eqtr4i	$⊢ 4 - 1 + 1 = 4$
125	121 124	syl6eq	$⊢ k = 1 \to 4 - k + 1 = 4$
126	119 125	oveq12d	$⊢ k = 1 \to \frac{k BernPoly X}{4 - k + 1} = \frac{1 BernPoly X}{4}$
127	118 126	oveq12d	$⊢ k = 1 \to (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1}) = 4 (\frac{1 BernPoly X}{4})$
128	114 127	sylbi	$⊢ k = 0 + 1 \to (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1}) = 4 (\frac{1 BernPoly X}{4})$
129	103 113 128	fsump1	$⊢ X \in ℂ \to \sum_{k = 0}^{0 + 1} (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1}) = \sum_{k = 0}^{0} (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1}) + 4 (\frac{1 BernPoly X}{4})$
130		0z	$⊢ 0 \in ℤ$
131	59	a1i	$⊢ X \in ℂ \to 1 \in ℂ$
132		bpolycl	$⊢ (0 \in ℕ_{0} \land X \in ℂ) \to 0 BernPoly X \in ℂ$
133	100 132	mpan	$⊢ X \in ℂ \to 0 BernPoly X \in ℂ$
134		5cn	$⊢ 5 \in ℂ$
135	134	a1i	$⊢ X \in ℂ \to 5 \in ℂ$
136		0re	$⊢ 0 \in ℝ$
137		5pos	$⊢ 0 < 5$
138	136 137	gtneii	$⊢ 5 \neq 0$
139	138	a1i	$⊢ X \in ℂ \to 5 \neq 0$
140	133 135 139	divcld	$⊢ X \in ℂ \to \frac{0 BernPoly X}{5} \in ℂ$
141	131 140	mulcld	$⊢ X \in ℂ \to 1 (\frac{0 BernPoly X}{5}) \in ℂ$
142		oveq2	$⊢ k = 0 \to (\binom{4}{k}) = (\binom{4}{0})$
143		bcn0	$⊢ 4 \in ℕ_{0} \to (\binom{4}{0}) = 1$
144	1 143	ax-mp	$⊢ (\binom{4}{0}) = 1$
145	142 144	syl6eq	$⊢ k = 0 \to (\binom{4}{k}) = 1$
146		oveq1	$⊢ k = 0 \to k BernPoly X = 0 BernPoly X$
147		oveq2	$⊢ k = 0 \to 4 - k = 4 - 0$
148	147	oveq1d	$⊢ k = 0 \to 4 - k + 1 = 4 - 0 + 1$
149	57	subid1i	$⊢ 4 - 0 = 4$
150	149	oveq1i	$⊢ 4 - 0 + 1 = 4 + 1$
151		4p1e5	$⊢ 4 + 1 = 5$
152	150 151	eqtri	$⊢ 4 - 0 + 1 = 5$
153	148 152	syl6eq	$⊢ k = 0 \to 4 - k + 1 = 5$
154	146 153	oveq12d	$⊢ k = 0 \to \frac{k BernPoly X}{4 - k + 1} = \frac{0 BernPoly X}{5}$
155	145 154	oveq12d	$⊢ k = 0 \to (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1}) = 1 (\frac{0 BernPoly X}{5})$
156	155	fsum1	$⊢ (0 \in ℤ \land 1 (\frac{0 BernPoly X}{5}) \in ℂ) \to \sum_{k = 0}^{0} (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1}) = 1 (\frac{0 BernPoly X}{5})$
157	130 141 156	sylancr	$⊢ X \in ℂ \to \sum_{k = 0}^{0} (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1}) = 1 (\frac{0 BernPoly X}{5})$
158		bpoly0	$⊢ X \in ℂ \to 0 BernPoly X = 1$
159	158	oveq1d	$⊢ X \in ℂ \to \frac{0 BernPoly X}{5} = \frac{1}{5}$
160	159	oveq2d	$⊢ X \in ℂ \to 1 (\frac{0 BernPoly X}{5}) = 1 (\frac{1}{5})$
161	134 138	reccli	$⊢ \frac{1}{5} \in ℂ$
162	161	mulid2i	$⊢ 1 (\frac{1}{5}) = \frac{1}{5}$
163	160 162	syl6eq	$⊢ X \in ℂ \to 1 (\frac{0 BernPoly X}{5}) = \frac{1}{5}$
164	157 163	eqtrd	$⊢ X \in ℂ \to \sum_{k = 0}^{0} (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1}) = \frac{1}{5}$
165		1nn0	$⊢ 1 \in ℕ_{0}$
166		bpolycl	$⊢ (1 \in ℕ_{0} \land X \in ℂ) \to 1 BernPoly X \in ℂ$
167	165 166	mpan	$⊢ X \in ℂ \to 1 BernPoly X \in ℂ$
168		nn0cn	$⊢ 4 \in ℕ_{0} \to 4 \in ℂ$
169	1 168	mp1i	$⊢ X \in ℂ \to 4 \in ℂ$
170		4ne0	$⊢ 4 \neq 0$
171	170	a1i	$⊢ X \in ℂ \to 4 \neq 0$
172	167 169 171	divcan2d	$⊢ X \in ℂ \to 4 (\frac{1 BernPoly X}{4}) = 1 BernPoly X$
173		bpoly1	$⊢ X \in ℂ \to 1 BernPoly X = X - (\frac{1}{2})$
174	172 173	eqtrd	$⊢ X \in ℂ \to 4 (\frac{1 BernPoly X}{4}) = X - (\frac{1}{2})$
175	164 174	oveq12d	$⊢ X \in ℂ \to \sum_{k = 0}^{0} (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1}) + 4 (\frac{1 BernPoly X}{4}) = (\frac{1}{5}) + X - (\frac{1}{2})$
176	129 175	eqtrd	$⊢ X \in ℂ \to \sum_{k = 0}^{0 + 1} (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1}) = (\frac{1}{5}) + X - (\frac{1}{2})$
177	99 176	syl5eqr	$⊢ X \in ℂ \to \sum_{k = 0}^{1} (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1}) = (\frac{1}{5}) + X - (\frac{1}{2})$
178		6cn	$⊢ 6 \in ℂ$
179	178	a1i	$⊢ X \in ℂ \to 6 \in ℂ$
180		2nn0	$⊢ 2 \in ℕ_{0}$
181		bpolycl	$⊢ (2 \in ℕ_{0} \land X \in ℂ) \to 2 BernPoly X \in ℂ$
182	180 181	mpan	$⊢ X \in ℂ \to 2 BernPoly X \in ℂ$
183	58	a1i	$⊢ X \in ℂ \to 3 \in ℂ$
184		3ne0	$⊢ 3 \neq 0$
185	184	a1i	$⊢ X \in ℂ \to 3 \neq 0$
186	179 182 183 185	div12d	$⊢ X \in ℂ \to 6 (\frac{2 BernPoly X}{3}) = (2 BernPoly X) (\frac{6}{3})$
187		3t2e6	$⊢ 3 \cdot 2 = 6$
188	178 58 87 184	divmuli	$⊢ \frac{6}{3} = 2 \leftrightarrow 3 \cdot 2 = 6$
189	187 188	mpbir	$⊢ \frac{6}{3} = 2$
190	189	oveq2i	$⊢ (2 BernPoly X) (\frac{6}{3}) = (2 BernPoly X) \cdot 2$
191	87	a1i	$⊢ X \in ℂ \to 2 \in ℂ$
192	182 191	mulcomd	$⊢ X \in ℂ \to (2 BernPoly X) \cdot 2 = 2 (2 BernPoly X)$
193		bpoly2	$⊢ X \in ℂ \to 2 BernPoly X = X^{2} - X + (\frac{1}{6})$
194	193	oveq2d	$⊢ X \in ℂ \to 2 (2 BernPoly X) = 2 (X^{2} - X + (\frac{1}{6}))$
195	192 194	eqtrd	$⊢ X \in ℂ \to (2 BernPoly X) \cdot 2 = 2 (X^{2} - X + (\frac{1}{6}))$
196	190 195	syl5eq	$⊢ X \in ℂ \to (2 BernPoly X) (\frac{6}{3}) = 2 (X^{2} - X + (\frac{1}{6}))$
197	186 196	eqtrd	$⊢ X \in ℂ \to 6 (\frac{2 BernPoly X}{3}) = 2 (X^{2} - X + (\frac{1}{6}))$
198	177 197	oveq12d	$⊢ X \in ℂ \to \sum_{k = 0}^{1} (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1}) + 6 (\frac{2 BernPoly X}{3}) = (\frac{1}{5}) + (X - (\frac{1}{2})) + 2 (X^{2} - X + (\frac{1}{6}))$
199	96 198	eqtrd	$⊢ X \in ℂ \to \sum_{k = 0}^{1 + 1} (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1}) = (\frac{1}{5}) + (X - (\frac{1}{2})) + 2 (X^{2} - X + (\frac{1}{6}))$
200	71 199	syl5eq	$⊢ X \in ℂ \to \sum_{k = 0}^{2} (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1}) = (\frac{1}{5}) + (X - (\frac{1}{2})) + 2 (X^{2} - X + (\frac{1}{6}))$
201		3nn0	$⊢ 3 \in ℕ_{0}$
202		bpolycl	$⊢ (3 \in ℕ_{0} \land X \in ℂ) \to 3 BernPoly X \in ℂ$
203	201 202	mpan	$⊢ X \in ℂ \to 3 BernPoly X \in ℂ$
204		2ne0	$⊢ 2 \neq 0$
205	204	a1i	$⊢ X \in ℂ \to 2 \neq 0$
206	169 203 191 205	div12d	$⊢ X \in ℂ \to 4 (\frac{3 BernPoly X}{2}) = (3 BernPoly X) (\frac{4}{2})$
207		4d2e2	$⊢ \frac{4}{2} = 2$
208	207	oveq2i	$⊢ (3 BernPoly X) (\frac{4}{2}) = (3 BernPoly X) \cdot 2$
209	203 191	mulcomd	$⊢ X \in ℂ \to (3 BernPoly X) \cdot 2 = 2 (3 BernPoly X)$
210		bpoly3	$⊢ X \in ℂ \to 3 BernPoly X = X^{3} - (\frac{3}{2}) X^{2} + (\frac{1}{2}) X$
211	210	oveq2d	$⊢ X \in ℂ \to 2 (3 BernPoly X) = 2 (X^{3} - (\frac{3}{2}) X^{2} + (\frac{1}{2}) X)$
212	209 211	eqtrd	$⊢ X \in ℂ \to (3 BernPoly X) \cdot 2 = 2 (X^{3} - (\frac{3}{2}) X^{2} + (\frac{1}{2}) X)$
213	208 212	syl5eq	$⊢ X \in ℂ \to (3 BernPoly X) (\frac{4}{2}) = 2 (X^{3} - (\frac{3}{2}) X^{2} + (\frac{1}{2}) X)$
214	206 213	eqtrd	$⊢ X \in ℂ \to 4 (\frac{3 BernPoly X}{2}) = 2 (X^{3} - (\frac{3}{2}) X^{2} + (\frac{1}{2}) X)$
215	200 214	oveq12d	$⊢ X \in ℂ \to \sum_{k = 0}^{2} (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1}) + 4 (\frac{3 BernPoly X}{2}) = ((\frac{1}{5}) + X - (\frac{1}{2})) + 2 (X^{2} - X + (\frac{1}{6})) + 2 (X^{3} - (\frac{3}{2}) X^{2} + (\frac{1}{2}) X)$
216	69 215	eqtrd	$⊢ X \in ℂ \to \sum_{k = 0}^{2 + 1} (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1}) = ((\frac{1}{5}) + X - (\frac{1}{2})) + 2 (X^{2} - X + (\frac{1}{6})) + 2 (X^{3} - (\frac{3}{2}) X^{2} + (\frac{1}{2}) X)$
217	8 216	syl5eq	$⊢ X \in ℂ \to \sum_{k = 0}^{4 - 1} (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1}) = ((\frac{1}{5}) + X - (\frac{1}{2})) + 2 (X^{2} - X + (\frac{1}{6})) + 2 (X^{3} - (\frac{3}{2}) X^{2} + (\frac{1}{2}) X)$
218	217	oveq2d	$⊢ X \in ℂ \to X^{4} - \sum_{k = 0}^{4 - 1} (\binom{4}{k}) (\frac{k BernPoly X}{4 - k + 1}) = X^{4} - (((\frac{1}{5}) + X - (\frac{1}{2})) + 2 (X^{2} - X + (\frac{1}{6})) + 2 (X^{3} - (\frac{3}{2}) X^{2} + (\frac{1}{2}) X))$
219		expcl	$⊢ (X \in ℂ \land 4 \in ℕ_{0}) \to X^{4} \in ℂ$
220	1 219	mpan2	$⊢ X \in ℂ \to X^{4} \in ℂ$
221		expcl	$⊢ (X \in ℂ \land 3 \in ℕ_{0}) \to X^{3} \in ℂ$
222	201 221	mpan2	$⊢ X \in ℂ \to X^{3} \in ℂ$
223	191 222	mulcld	$⊢ X \in ℂ \to 2 X^{3} \in ℂ$
224		sqcl	$⊢ X \in ℂ \to X^{2} \in ℂ$
225	201 100	deccl	$⊢ 30 \in ℕ_{0}$
226	225	nn0cni	$⊢ 30 \in ℂ$
227		dfdec10	$⊢ 30 = 10 \cdot 3 + 0$
228		10re	$⊢ 10 \in ℝ$
229	228	recni	$⊢ 10 \in ℂ$
230	229 58	mulcli	$⊢ 10 \cdot 3 \in ℂ$
231	230	addid1i	$⊢ 10 \cdot 3 + 0 = 10 \cdot 3$
232	227 231	eqtri	$⊢ 30 = 10 \cdot 3$
233		10pos	$⊢ 0 < 10$
234	136 233	gtneii	$⊢ 10 \neq 0$
235	229 58 234 184	mulne0i	$⊢ 10 \cdot 3 \neq 0$
236	232 235	eqnetri	$⊢ 30 \neq 0$
237	226 236	reccli	$⊢ \frac{1}{30} \in ℂ$
238	237	a1i	$⊢ X \in ℂ \to \frac{1}{30} \in ℂ$
239	224 238	subcld	$⊢ X \in ℂ \to X^{2} - (\frac{1}{30}) \in ℂ$
240	220 223 239	subsubd	$⊢ X \in ℂ \to X^{4} - (2 X^{3} - (X^{2} - (\frac{1}{30}))) = (X^{4} - 2 X^{3}) + X^{2} - (\frac{1}{30})$
241	161	a1i	$⊢ X \in ℂ \to \frac{1}{5} \in ℂ$
242		id	$⊢ X \in ℂ \to X \in ℂ$
243	87 204	reccli	$⊢ \frac{1}{2} \in ℂ$
244	243	a1i	$⊢ X \in ℂ \to \frac{1}{2} \in ℂ$
245	242 244	subcld	$⊢ X \in ℂ \to X - (\frac{1}{2}) \in ℂ$
246	241 245	addcld	$⊢ X \in ℂ \to (\frac{1}{5}) + X - (\frac{1}{2}) \in ℂ$
247	224 242	subcld	$⊢ X \in ℂ \to X^{2} - X \in ℂ$
248		6pos	$⊢ 0 < 6$
249	136 248	gtneii	$⊢ 6 \neq 0$
250	178 249	reccli	$⊢ \frac{1}{6} \in ℂ$
251	250	a1i	$⊢ X \in ℂ \to \frac{1}{6} \in ℂ$
252	247 251	addcld	$⊢ X \in ℂ \to X^{2} - X + (\frac{1}{6}) \in ℂ$
253	191 252	mulcld	$⊢ X \in ℂ \to 2 (X^{2} - X + (\frac{1}{6})) \in ℂ$
254	246 253	addcld	$⊢ X \in ℂ \to (\frac{1}{5}) + (X - (\frac{1}{2})) + 2 (X^{2} - X + (\frac{1}{6})) \in ℂ$
255	58 87 204	divcli	$⊢ \frac{3}{2} \in ℂ$
256	255	a1i	$⊢ X \in ℂ \to \frac{3}{2} \in ℂ$
257	256 224	mulcld	$⊢ X \in ℂ \to (\frac{3}{2}) X^{2} \in ℂ$
258	222 257	subcld	$⊢ X \in ℂ \to X^{3} - (\frac{3}{2}) X^{2} \in ℂ$
259	244 242	mulcld	$⊢ X \in ℂ \to (\frac{1}{2}) X \in ℂ$
260	258 259	addcld	$⊢ X \in ℂ \to X^{3} - (\frac{3}{2}) X^{2} + (\frac{1}{2}) X \in ℂ$
261	191 260	mulcld	$⊢ X \in ℂ \to 2 (X^{3} - (\frac{3}{2}) X^{2} + (\frac{1}{2}) X) \in ℂ$
262	254 261	addcomd	$⊢ X \in ℂ \to ((\frac{1}{5}) + X - (\frac{1}{2})) + 2 (X^{2} - X + (\frac{1}{6})) + 2 (X^{3} - (\frac{3}{2}) X^{2} + (\frac{1}{2}) X) = 2 (X^{3} - (\frac{3}{2}) X^{2} + (\frac{1}{2}) X) + ((\frac{1}{5}) + X - (\frac{1}{2})) + 2 (X^{2} - X + (\frac{1}{6}))$
263	191 258 259	adddid	$⊢ X \in ℂ \to 2 (X^{3} - (\frac{3}{2}) X^{2} + (\frac{1}{2}) X) = 2 (X^{3} - (\frac{3}{2}) X^{2}) + 2 (\frac{1}{2}) X$
264	191 222 257	subdid	$⊢ X \in ℂ \to 2 (X^{3} - (\frac{3}{2}) X^{2}) = 2 X^{3} - 2 (\frac{3}{2}) X^{2}$
265	87 204	recidi	$⊢ 2 (\frac{1}{2}) = 1$
266	265	oveq1i	$⊢ 2 (\frac{1}{2}) X = 1 X$
267	191 244 242	mulassd	$⊢ X \in ℂ \to 2 (\frac{1}{2}) X = 2 (\frac{1}{2}) X$
268		mulid2	$⊢ X \in ℂ \to 1 X = X$
269	266 267 268	3eqtr3a	$⊢ X \in ℂ \to 2 (\frac{1}{2}) X = X$
270	264 269	oveq12d	$⊢ X \in ℂ \to 2 (X^{3} - (\frac{3}{2}) X^{2}) + 2 (\frac{1}{2}) X = 2 X^{3} - 2 (\frac{3}{2}) X^{2} + X$
271	263 270	eqtrd	$⊢ X \in ℂ \to 2 (X^{3} - (\frac{3}{2}) X^{2} + (\frac{1}{2}) X) = 2 X^{3} - 2 (\frac{3}{2}) X^{2} + X$
272	271	oveq1d	$⊢ X \in ℂ \to 2 (X^{3} - (\frac{3}{2}) X^{2} + (\frac{1}{2}) X) + ((\frac{1}{5}) + X - (\frac{1}{2})) + 2 (X^{2} - X + (\frac{1}{6})) = (2 X^{3} - 2 (\frac{3}{2}) X^{2}) + X + ((\frac{1}{5}) + X - (\frac{1}{2})) + 2 (X^{2} - X + (\frac{1}{6}))$
273	191 257	mulcld	$⊢ X \in ℂ \to 2 (\frac{3}{2}) X^{2} \in ℂ$
274	223 273	subcld	$⊢ X \in ℂ \to 2 X^{3} - 2 (\frac{3}{2}) X^{2} \in ℂ$
275	274 242 254	addassd	$⊢ X \in ℂ \to (2 X^{3} - 2 (\frac{3}{2}) X^{2}) + X + ((\frac{1}{5}) + X - (\frac{1}{2})) + 2 (X^{2} - X + (\frac{1}{6})) = (2 X^{3} - 2 (\frac{3}{2}) X^{2}) + X + ((\frac{1}{5}) + (X - (\frac{1}{2})) + 2 (X^{2} - X + (\frac{1}{6})))$
276	242 254	addcld	$⊢ X \in ℂ \to X + ((\frac{1}{5}) + X - (\frac{1}{2})) + 2 (X^{2} - X + (\frac{1}{6})) \in ℂ$
277	223 273 276	subsubd	$⊢ X \in ℂ \to 2 X^{3} - (2 (\frac{3}{2}) X^{2} - (X + ((\frac{1}{5}) + X - (\frac{1}{2})) + 2 (X^{2} - X + (\frac{1}{6})))) = (2 X^{3} - 2 (\frac{3}{2}) X^{2}) + X + ((\frac{1}{5}) + (X - (\frac{1}{2})) + 2 (X^{2} - X + (\frac{1}{6})))$
278	58 87 204	divcan2i	$⊢ 2 (\frac{3}{2}) = 3$
279	278	oveq1i	$⊢ 2 (\frac{3}{2}) X^{2} = 3 X^{2}$
280	191 256 224	mulassd	$⊢ X \in ℂ \to 2 (\frac{3}{2}) X^{2} = 2 (\frac{3}{2}) X^{2}$
281	279 280	syl5reqr	$⊢ X \in ℂ \to 2 (\frac{3}{2}) X^{2} = 3 X^{2}$
282	281	oveq1d	$⊢ X \in ℂ \to 2 (\frac{3}{2}) X^{2} - (X + ((\frac{1}{5}) + X - (\frac{1}{2})) + 2 (X^{2} - X + (\frac{1}{6}))) = 3 X^{2} - (X + ((\frac{1}{5}) + X - (\frac{1}{2})) + 2 (X^{2} - X + (\frac{1}{6})))$
283	242 246 253	add12d	$⊢ X \in ℂ \to X + ((\frac{1}{5}) + X - (\frac{1}{2})) + 2 (X^{2} - X + (\frac{1}{6})) = (\frac{1}{5}) + (X - (\frac{1}{2})) + X + 2 (X^{2} - X + (\frac{1}{6}))$
284	191 247 251	adddid	$⊢ X \in ℂ \to 2 (X^{2} - X + (\frac{1}{6})) = 2 (X^{2} - X) + 2 (\frac{1}{6})$
285	191 224 242	subdid	$⊢ X \in ℂ \to 2 (X^{2} - X) = 2 X^{2} - 2 X$
286	187	oveq2i	$⊢ \frac{2}{3 \cdot 2} = \frac{2}{6}$
287	58 184	reccli	$⊢ \frac{1}{3} \in ℂ$
288	58 87 287	mul32i	$⊢ 3 \cdot 2 (\frac{1}{3}) = 3 (\frac{1}{3}) \cdot 2$
289	58 184	recidi	$⊢ 3 (\frac{1}{3}) = 1$
290	289	oveq1i	$⊢ 3 (\frac{1}{3}) \cdot 2 = 1 \cdot 2$
291	87	mulid2i	$⊢ 1 \cdot 2 = 2$
292	290 291	eqtri	$⊢ 3 (\frac{1}{3}) \cdot 2 = 2$
293	288 292	eqtri	$⊢ 3 \cdot 2 (\frac{1}{3}) = 2$
294	187 178	eqeltri	$⊢ 3 \cdot 2 \in ℂ$
295	187 249	eqnetri	$⊢ 3 \cdot 2 \neq 0$
296	87 294 287 295	divmuli	$⊢ \frac{2}{3 \cdot 2} = \frac{1}{3} \leftrightarrow 3 \cdot 2 (\frac{1}{3}) = 2$
297	293 296	mpbir	$⊢ \frac{2}{3 \cdot 2} = \frac{1}{3}$
298	87 178 249	divreci	$⊢ \frac{2}{6} = 2 (\frac{1}{6})$
299	286 297 298	3eqtr3ri	$⊢ 2 (\frac{1}{6}) = \frac{1}{3}$
300	299	a1i	$⊢ X \in ℂ \to 2 (\frac{1}{6}) = \frac{1}{3}$
301	285 300	oveq12d	$⊢ X \in ℂ \to 2 (X^{2} - X) + 2 (\frac{1}{6}) = 2 X^{2} - 2 X + (\frac{1}{3})$
302	284 301	eqtrd	$⊢ X \in ℂ \to 2 (X^{2} - X + (\frac{1}{6})) = 2 X^{2} - 2 X + (\frac{1}{3})$
303	302	oveq2d	$⊢ X \in ℂ \to X + 2 (X^{2} - X + (\frac{1}{6})) = X + (2 X^{2} - 2 X) + (\frac{1}{3})$
304	191 224	mulcld	$⊢ X \in ℂ \to 2 X^{2} \in ℂ$
305	191 242	mulcld	$⊢ X \in ℂ \to 2 X \in ℂ$
306	304 305	subcld	$⊢ X \in ℂ \to 2 X^{2} - 2 X \in ℂ$
307	287	a1i	$⊢ X \in ℂ \to \frac{1}{3} \in ℂ$
308	242 306 307	addassd	$⊢ X \in ℂ \to X + (2 X^{2} - 2 X) + (\frac{1}{3}) = X + (2 X^{2} - 2 X) + (\frac{1}{3})$
309	242 304 305	addsub12d	$⊢ X \in ℂ \to X + 2 X^{2} - 2 X = 2 X^{2} + X - 2 X$
310	309	oveq1d	$⊢ X \in ℂ \to X + (2 X^{2} - 2 X) + (\frac{1}{3}) = 2 X^{2} + (X - 2 X) + (\frac{1}{3})$
311	303 308 310	3eqtr2d	$⊢ X \in ℂ \to X + 2 (X^{2} - X + (\frac{1}{6})) = 2 X^{2} + (X - 2 X) + (\frac{1}{3})$
312	311	oveq2d	$⊢ X \in ℂ \to (\frac{1}{5}) + (X - (\frac{1}{2})) + X + 2 (X^{2} - X + (\frac{1}{6})) = (\frac{1}{5}) + (X - (\frac{1}{2})) + (2 X^{2} + X - 2 X) + (\frac{1}{3})$
313	283 312	eqtrd	$⊢ X \in ℂ \to X + ((\frac{1}{5}) + X - (\frac{1}{2})) + 2 (X^{2} - X + (\frac{1}{6})) = (\frac{1}{5}) + (X - (\frac{1}{2})) + (2 X^{2} + X - 2 X) + (\frac{1}{3})$
314	313	oveq2d	$⊢ X \in ℂ \to 3 X^{2} - (X + ((\frac{1}{5}) + X - (\frac{1}{2})) + 2 (X^{2} - X + (\frac{1}{6}))) = 3 X^{2} - ((\frac{1}{5}) + (X - (\frac{1}{2})) + (2 X^{2} + X - 2 X) + (\frac{1}{3}))$
315	242 305	subcld	$⊢ X \in ℂ \to X - 2 X \in ℂ$
316	304 315	addcld	$⊢ X \in ℂ \to 2 X^{2} + X - 2 X \in ℂ$
317	241 245 316 307	add4d	$⊢ X \in ℂ \to (\frac{1}{5}) + (X - (\frac{1}{2})) + (2 X^{2} + X - 2 X) + (\frac{1}{3}) = (\frac{1}{5}) + (2 X^{2} + X - 2 X) + (X - (\frac{1}{2})) + (\frac{1}{3})$
318	241 304 315	add12d	$⊢ X \in ℂ \to (\frac{1}{5}) + 2 X^{2} + (X - 2 X) = 2 X^{2} + (\frac{1}{5}) + (X - 2 X)$
319	318	oveq1d	$⊢ X \in ℂ \to (\frac{1}{5}) + (2 X^{2} + X - 2 X) + (X - (\frac{1}{2})) + (\frac{1}{3}) = 2 X^{2} + ((\frac{1}{5}) + X - 2 X) + (X - (\frac{1}{2})) + (\frac{1}{3})$
320	241 315	addcld	$⊢ X \in ℂ \to (\frac{1}{5}) + X - 2 X \in ℂ$
321	245 307	addcld	$⊢ X \in ℂ \to X - (\frac{1}{2}) + (\frac{1}{3}) \in ℂ$
322	304 320 321	addassd	$⊢ X \in ℂ \to 2 X^{2} + ((\frac{1}{5}) + X - 2 X) + (X - (\frac{1}{2})) + (\frac{1}{3}) = 2 X^{2} + ((\frac{1}{5}) + X - 2 X) + (X - (\frac{1}{2}) + (\frac{1}{3}))$
323	317 319 322	3eqtrd	$⊢ X \in ℂ \to (\frac{1}{5}) + (X - (\frac{1}{2})) + (2 X^{2} + X - 2 X) + (\frac{1}{3}) = 2 X^{2} + ((\frac{1}{5}) + X - 2 X) + (X - (\frac{1}{2}) + (\frac{1}{3}))$
324	323	oveq2d	$⊢ X \in ℂ \to 3 X^{2} - ((\frac{1}{5}) + (X - (\frac{1}{2})) + (2 X^{2} + X - 2 X) + (\frac{1}{3})) = 3 X^{2} - (2 X^{2} + ((\frac{1}{5}) + X - 2 X) + (X - (\frac{1}{2}) + (\frac{1}{3})))$
325	183 224	mulcld	$⊢ X \in ℂ \to 3 X^{2} \in ℂ$
326	320 321	addcld	$⊢ X \in ℂ \to (\frac{1}{5}) + (X - 2 X) + (X - (\frac{1}{2})) + (\frac{1}{3}) \in ℂ$
327	325 304 326	subsub4d	$⊢ X \in ℂ \to 3 X^{2} - 2 X^{2} - ((\frac{1}{5}) + (X - 2 X) + (X - (\frac{1}{2})) + (\frac{1}{3})) = 3 X^{2} - (2 X^{2} + ((\frac{1}{5}) + X - 2 X) + (X - (\frac{1}{2}) + (\frac{1}{3})))$
328	58 87 59 109	subaddrii	$⊢ 3 - 2 = 1$
329	328	oveq1i	$⊢ (3 - 2) X^{2} = 1 X^{2}$
330	183 191 224	subdird	$⊢ X \in ℂ \to (3 - 2) X^{2} = 3 X^{2} - 2 X^{2}$
331	224	mulid2d	$⊢ X \in ℂ \to 1 X^{2} = X^{2}$
332	329 330 331	3eqtr3a	$⊢ X \in ℂ \to 3 X^{2} - 2 X^{2} = X^{2}$
333	241 305 242	subsubd	$⊢ X \in ℂ \to (\frac{1}{5}) - (2 X - X) = (\frac{1}{5}) - 2 X + X$
334		2txmxeqx	$⊢ X \in ℂ \to 2 X - X = X$
335	334	oveq2d	$⊢ X \in ℂ \to (\frac{1}{5}) - (2 X - X) = (\frac{1}{5}) - X$
336	241 305 242	subadd23d	$⊢ X \in ℂ \to (\frac{1}{5}) - 2 X + X = (\frac{1}{5}) + X - 2 X$
337	333 335 336	3eqtr3d	$⊢ X \in ℂ \to (\frac{1}{5}) - X = (\frac{1}{5}) + X - 2 X$
338	242 244 307	subsubd	$⊢ X \in ℂ \to X - ((\frac{1}{2}) - (\frac{1}{3})) = X - (\frac{1}{2}) + (\frac{1}{3})$
339	337 338	oveq12d	$⊢ X \in ℂ \to ((\frac{1}{5}) - X) + X - ((\frac{1}{2}) - (\frac{1}{3})) = (\frac{1}{5}) + (X - 2 X) + (X - (\frac{1}{2})) + (\frac{1}{3})$
340	243 287	subcli	$⊢ (\frac{1}{2}) - (\frac{1}{3}) \in ℂ$
341	340	a1i	$⊢ X \in ℂ \to (\frac{1}{2}) - (\frac{1}{3}) \in ℂ$
342	241 242 341	npncand	$⊢ X \in ℂ \to ((\frac{1}{5}) - X) + X - ((\frac{1}{2}) - (\frac{1}{3})) = (\frac{1}{5}) - ((\frac{1}{2}) - (\frac{1}{3}))$
343		halfthird	$⊢ (\frac{1}{2}) - (\frac{1}{3}) = \frac{1}{6}$
344	343	oveq2i	$⊢ (\frac{1}{5}) - ((\frac{1}{2}) - (\frac{1}{3})) = (\frac{1}{5}) - (\frac{1}{6})$
345		5recm6rec	$⊢ (\frac{1}{5}) - (\frac{1}{6}) = \frac{1}{30}$
346	344 345	eqtri	$⊢ (\frac{1}{5}) - ((\frac{1}{2}) - (\frac{1}{3})) = \frac{1}{30}$
347	342 346	syl6eq	$⊢ X \in ℂ \to ((\frac{1}{5}) - X) + X - ((\frac{1}{2}) - (\frac{1}{3})) = \frac{1}{30}$
348	339 347	eqtr3d	$⊢ X \in ℂ \to (\frac{1}{5}) + (X - 2 X) + (X - (\frac{1}{2})) + (\frac{1}{3}) = \frac{1}{30}$
349	332 348	oveq12d	$⊢ X \in ℂ \to 3 X^{2} - 2 X^{2} - ((\frac{1}{5}) + (X - 2 X) + (X - (\frac{1}{2})) + (\frac{1}{3})) = X^{2} - (\frac{1}{30})$
350	324 327 349	3eqtr2d	$⊢ X \in ℂ \to 3 X^{2} - ((\frac{1}{5}) + (X - (\frac{1}{2})) + (2 X^{2} + X - 2 X) + (\frac{1}{3})) = X^{2} - (\frac{1}{30})$
351	282 314 350	3eqtrd	$⊢ X \in ℂ \to 2 (\frac{3}{2}) X^{2} - (X + ((\frac{1}{5}) + X - (\frac{1}{2})) + 2 (X^{2} - X + (\frac{1}{6}))) = X^{2} - (\frac{1}{30})$
352	351	oveq2d	$⊢ X \in ℂ \to 2 X^{3} - (2 (\frac{3}{2}) X^{2} - (X + ((\frac{1}{5}) + X - (\frac{1}{2})) + 2 (X^{2} - X + (\frac{1}{6})))) = 2 X^{3} - (X^{2} - (\frac{1}{30}))$
353	275 277 352	3eqtr2d	$⊢ X \in ℂ \to (2 X^{3} - 2 (\frac{3}{2}) X^{2}) + X + ((\frac{1}{5}) + X - (\frac{1}{2})) + 2 (X^{2} - X + (\frac{1}{6})) = 2 X^{3} - (X^{2} - (\frac{1}{30}))$
354	262 272 353	3eqtrd	$⊢ X \in ℂ \to ((\frac{1}{5}) + X - (\frac{1}{2})) + 2 (X^{2} - X + (\frac{1}{6})) + 2 (X^{3} - (\frac{3}{2}) X^{2} + (\frac{1}{2}) X) = 2 X^{3} - (X^{2} - (\frac{1}{30}))$
355	354	oveq2d	$⊢ X \in ℂ \to X^{4} - (((\frac{1}{5}) + X - (\frac{1}{2})) + 2 (X^{2} - X + (\frac{1}{6})) + 2 (X^{3} - (\frac{3}{2}) X^{2} + (\frac{1}{2}) X)) = X^{4} - (2 X^{3} - (X^{2} - (\frac{1}{30})))$
356	220 223	subcld	$⊢ X \in ℂ \to X^{4} - 2 X^{3} \in ℂ$
357	356 224 238	addsubassd	$⊢ X \in ℂ \to (X^{4} - 2 X^{3}) + X^{2} - (\frac{1}{30}) = (X^{4} - 2 X^{3}) + X^{2} - (\frac{1}{30})$
358	240 355 357	3eqtr4d	$⊢ X \in ℂ \to X^{4} - (((\frac{1}{5}) + X - (\frac{1}{2})) + 2 (X^{2} - X + (\frac{1}{6})) + 2 (X^{3} - (\frac{3}{2}) X^{2} + (\frac{1}{2}) X)) = (X^{4} - 2 X^{3}) + X^{2} - (\frac{1}{30})$
359	3 218 358	3eqtrd	$⊢ X \in ℂ \to 4 BernPoly X = (X^{4} - 2 X^{3}) + X^{2} - (\frac{1}{30})$

Metamath Proof Explorer

Theorem bpoly4

Proof