Theorem bpoly4

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

	Ref	Expression
Assertion	bpoly4	⊢ ( 𝑋 ∈ ℂ → ( 4 BernPoly 𝑋 ) = ( ( ( ( 𝑋 ↑ 4 ) − ( 2 · ( 𝑋 ↑ 3 ) ) ) + ( 𝑋 ↑ 2 ) ) − ( 1 / ; 3 0 ) ) )

Proof

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