Theorem bpoly3

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

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

Proof

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