bpoly4 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > bpoly4		Structured version Visualization version GIF version

Theorem bpoly4 14790

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

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

Proof of Theorem bpoly4 Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		4nn0 11311	. . 3 ⊢ 4 ∈ ℕ₀
2		bpolyval 14780	. . 3 ⊢ ((4 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → (4 BernPoly 𝑋) = ((𝑋↑4) − Σ𝑘 ∈ (0...(4 − 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)))))
3	1, 2	mpan 706	. 2 ⊢ (𝑋 ∈ ℂ → (4 BernPoly 𝑋) = ((𝑋↑4) − Σ𝑘 ∈ (0...(4 − 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)))))
4		4m1e3 11138	. . . . . . 7 ⊢ (4 − 1) = 3
5		df-3 11080	. . . . . . 7 ⊢ 3 = (2 + 1)
6	4, 5	eqtri 2644	. . . . . 6 ⊢ (4 − 1) = (2 + 1)
7	6	oveq2i 6661	. . . . 5 ⊢ (0...(4 − 1)) = (0...(2 + 1))
8	7	sumeq1i 14428	. . . 4 ⊢ Σ𝑘 ∈ (0...(4 − 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = Σ𝑘 ∈ (0...(2 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)))
9		2eluzge0 11733	. . . . . . 7 ⊢ 2 ∈ (ℤ_≥‘0)
10	9	a1i 11	. . . . . 6 ⊢ (𝑋 ∈ ℂ → 2 ∈ (ℤ_≥‘0))
11		elfzelz 12342	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...(2 + 1)) → 𝑘 ∈ ℤ)
12		bccl 13109	. . . . . . . . . 10 ⊢ ((4 ∈ ℕ₀ ∧ 𝑘 ∈ ℤ) → (4C𝑘) ∈ ℕ₀)
13	1, 11, 12	sylancr 695	. . . . . . . . 9 ⊢ (𝑘 ∈ (0...(2 + 1)) → (4C𝑘) ∈ ℕ₀)
14	13	nn0cnd 11353	. . . . . . . 8 ⊢ (𝑘 ∈ (0...(2 + 1)) → (4C𝑘) ∈ ℂ)
15	14	adantl 482	. . . . . . 7 ⊢ ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(2 + 1))) → (4C𝑘) ∈ ℂ)
16		elfznn0 12433	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...(2 + 1)) → 𝑘 ∈ ℕ₀)
17		bpolycl 14783	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → (𝑘 BernPoly 𝑋) ∈ ℂ)
18	16, 17	sylan 488	. . . . . . . . 9 ⊢ ((𝑘 ∈ (0...(2 + 1)) ∧ 𝑋 ∈ ℂ) → (𝑘 BernPoly 𝑋) ∈ ℂ)
19	18	ancoms 469	. . . . . . . 8 ⊢ ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(2 + 1))) → (𝑘 BernPoly 𝑋) ∈ ℂ)
20		4re 11097	. . . . . . . . . . . . 13 ⊢ 4 ∈ ℝ
21	20	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...(2 + 1)) → 4 ∈ ℝ)
22	11	zred 11482	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...(2 + 1)) → 𝑘 ∈ ℝ)
23	21, 22	resubcld 10458	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (0...(2 + 1)) → (4 − 𝑘) ∈ ℝ)
24		peano2re 10209	. . . . . . . . . . 11 ⊢ ((4 − 𝑘) ∈ ℝ → ((4 − 𝑘) + 1) ∈ ℝ)
25	23, 24	syl 17	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...(2 + 1)) → ((4 − 𝑘) + 1) ∈ ℝ)
26	25	recnd 10068	. . . . . . . . 9 ⊢ (𝑘 ∈ (0...(2 + 1)) → ((4 − 𝑘) + 1) ∈ ℂ)
27	26	adantl 482	. . . . . . . 8 ⊢ ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(2 + 1))) → ((4 − 𝑘) + 1) ∈ ℂ)
28		1red 10055	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (0...(2 + 1)) → 1 ∈ ℝ)
29	5	oveq2i 6661	. . . . . . . . . . . . . 14 ⊢ (0...3) = (0...(2 + 1))
30	29	eleq2i 2693	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (0...3) ↔ 𝑘 ∈ (0...(2 + 1)))
31		elfzelz 12342	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (0...3) → 𝑘 ∈ ℤ)
32	31	zred 11482	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...3) → 𝑘 ∈ ℝ)
33		3re 11094	. . . . . . . . . . . . . . 15 ⊢ 3 ∈ ℝ
34	33	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...3) → 3 ∈ ℝ)
35	20	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...3) → 4 ∈ ℝ)
36		elfzle2 12345	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...3) → 𝑘 ≤ 3)
37		3lt4 11197	. . . . . . . . . . . . . . 15 ⊢ 3 < 4
38	37	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...3) → 3 < 4)
39	32, 34, 35, 36, 38	lelttrd 10195	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (0...3) → 𝑘 < 4)
40	30, 39	sylbir 225	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...(2 + 1)) → 𝑘 < 4)
41	22, 21	posdifd 10614	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (0...(2 + 1)) → (𝑘 < 4 ↔ 0 < (4 − 𝑘)))
42	40, 41	mpbid 222	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (0...(2 + 1)) → 0 < (4 − 𝑘))
43		0lt1 10550	. . . . . . . . . . . 12 ⊢ 0 < 1
44	43	a1i 11	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (0...(2 + 1)) → 0 < 1)
45	23, 28, 42, 44	addgt0d 10602	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...(2 + 1)) → 0 < ((4 − 𝑘) + 1))
46	45	gt0ne0d 10592	. . . . . . . . 9 ⊢ (𝑘 ∈ (0...(2 + 1)) → ((4 − 𝑘) + 1) ≠ 0)
47	46	adantl 482	. . . . . . . 8 ⊢ ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(2 + 1))) → ((4 − 𝑘) + 1) ≠ 0)
48	19, 27, 47	divcld 10801	. . . . . . 7 ⊢ ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(2 + 1))) → ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)) ∈ ℂ)
49	15, 48	mulcld 10060	. . . . . 6 ⊢ ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(2 + 1))) → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) ∈ ℂ)
50	5	eqeq2i 2634	. . . . . . 7 ⊢ (𝑘 = 3 ↔ 𝑘 = (2 + 1))
51		oveq2 6658	. . . . . . . . 9 ⊢ (𝑘 = 3 → (4C𝑘) = (4C3))
52		4bc3eq4 13115	. . . . . . . . 9 ⊢ (4C3) = 4
53	51, 52	syl6eq 2672	. . . . . . . 8 ⊢ (𝑘 = 3 → (4C𝑘) = 4)
54		oveq1 6657	. . . . . . . . 9 ⊢ (𝑘 = 3 → (𝑘 BernPoly 𝑋) = (3 BernPoly 𝑋))
55		oveq2 6658	. . . . . . . . . . 11 ⊢ (𝑘 = 3 → (4 − 𝑘) = (4 − 3))
56	55	oveq1d 6665	. . . . . . . . . 10 ⊢ (𝑘 = 3 → ((4 − 𝑘) + 1) = ((4 − 3) + 1))
57		4cn 11098	. . . . . . . . . . . . 13 ⊢ 4 ∈ ℂ
58		3cn 11095	. . . . . . . . . . . . 13 ⊢ 3 ∈ ℂ
59		ax-1cn 9994	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
60		3p1e4 11153	. . . . . . . . . . . . 13 ⊢ (3 + 1) = 4
61	57, 58, 59, 60	subaddrii 10370	. . . . . . . . . . . 12 ⊢ (4 − 3) = 1
62	61	oveq1i 6660	. . . . . . . . . . 11 ⊢ ((4 − 3) + 1) = (1 + 1)
63		df-2 11079	. . . . . . . . . . 11 ⊢ 2 = (1 + 1)
64	62, 63	eqtr4i 2647	. . . . . . . . . 10 ⊢ ((4 − 3) + 1) = 2
65	56, 64	syl6eq 2672	. . . . . . . . 9 ⊢ (𝑘 = 3 → ((4 − 𝑘) + 1) = 2)
66	54, 65	oveq12d 6668	. . . . . . . 8 ⊢ (𝑘 = 3 → ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)) = ((3 BernPoly 𝑋) / 2))
67	53, 66	oveq12d 6668	. . . . . . 7 ⊢ (𝑘 = 3 → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (4 · ((3 BernPoly 𝑋) / 2)))
68	50, 67	sylbir 225	. . . . . 6 ⊢ (𝑘 = (2 + 1) → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (4 · ((3 BernPoly 𝑋) / 2)))
69	10, 49, 68	fsump1 14487	. . . . 5 ⊢ (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...(2 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (Σ𝑘 ∈ (0...2)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) + (4 · ((3 BernPoly 𝑋) / 2))))
70	63	oveq2i 6661	. . . . . . . 8 ⊢ (0...2) = (0...(1 + 1))
71	70	sumeq1i 14428	. . . . . . 7 ⊢ Σ𝑘 ∈ (0...2)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = Σ𝑘 ∈ (0...(1 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)))
72		1eluzge0 11732	. . . . . . . . . 10 ⊢ 1 ∈ (ℤ_≥‘0)
73	72	a1i 11	. . . . . . . . 9 ⊢ (𝑋 ∈ ℂ → 1 ∈ (ℤ_≥‘0))
74		fzssp1 12384	. . . . . . . . . . . 12 ⊢ (0...(1 + 1)) ⊆ (0...((1 + 1) + 1))
75	63	oveq1i 6660	. . . . . . . . . . . . 13 ⊢ (2 + 1) = ((1 + 1) + 1)
76	75	oveq2i 6661	. . . . . . . . . . . 12 ⊢ (0...(2 + 1)) = (0...((1 + 1) + 1))
77	74, 76	sseqtr4i 3638	. . . . . . . . . . 11 ⊢ (0...(1 + 1)) ⊆ (0...(2 + 1))
78	77	sseli 3599	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...(1 + 1)) → 𝑘 ∈ (0...(2 + 1)))
79	78, 49	sylan2 491	. . . . . . . . 9 ⊢ ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(1 + 1))) → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) ∈ ℂ)
80	63	eqeq2i 2634	. . . . . . . . . 10 ⊢ (𝑘 = 2 ↔ 𝑘 = (1 + 1))
81		oveq2 6658	. . . . . . . . . . . 12 ⊢ (𝑘 = 2 → (4C𝑘) = (4C2))
82		4bc2eq6 13116	. . . . . . . . . . . 12 ⊢ (4C2) = 6
83	81, 82	syl6eq 2672	. . . . . . . . . . 11 ⊢ (𝑘 = 2 → (4C𝑘) = 6)
84		oveq1 6657	. . . . . . . . . . . 12 ⊢ (𝑘 = 2 → (𝑘 BernPoly 𝑋) = (2 BernPoly 𝑋))
85		oveq2 6658	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 2 → (4 − 𝑘) = (4 − 2))
86	85	oveq1d 6665	. . . . . . . . . . . . 13 ⊢ (𝑘 = 2 → ((4 − 𝑘) + 1) = ((4 − 2) + 1))
87		2cn 11091	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℂ
88		2p2e4 11144	. . . . . . . . . . . . . . . 16 ⊢ (2 + 2) = 4
89	57, 87, 87, 88	subaddrii 10370	. . . . . . . . . . . . . . 15 ⊢ (4 − 2) = 2
90	89	oveq1i 6660	. . . . . . . . . . . . . 14 ⊢ ((4 − 2) + 1) = (2 + 1)
91	90, 5	eqtr4i 2647	. . . . . . . . . . . . 13 ⊢ ((4 − 2) + 1) = 3
92	86, 91	syl6eq 2672	. . . . . . . . . . . 12 ⊢ (𝑘 = 2 → ((4 − 𝑘) + 1) = 3)
93	84, 92	oveq12d 6668	. . . . . . . . . . 11 ⊢ (𝑘 = 2 → ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)) = ((2 BernPoly 𝑋) / 3))
94	83, 93	oveq12d 6668	. . . . . . . . . 10 ⊢ (𝑘 = 2 → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (6 · ((2 BernPoly 𝑋) / 3)))
95	80, 94	sylbir 225	. . . . . . . . 9 ⊢ (𝑘 = (1 + 1) → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (6 · ((2 BernPoly 𝑋) / 3)))
96	73, 79, 95	fsump1 14487	. . . . . . . 8 ⊢ (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...(1 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (Σ𝑘 ∈ (0...1)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) + (6 · ((2 BernPoly 𝑋) / 3))))
97		0p1e1 11132	. . . . . . . . . . . 12 ⊢ (0 + 1) = 1
98	97	oveq2i 6661	. . . . . . . . . . 11 ⊢ (0...(0 + 1)) = (0...1)
99	98	sumeq1i 14428	. . . . . . . . . 10 ⊢ Σ𝑘 ∈ (0...(0 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = Σ𝑘 ∈ (0...1)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)))
100		0nn0 11307	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℕ₀
101		nn0uz 11722	. . . . . . . . . . . . . 14 ⊢ ℕ₀ = (ℤ_≥‘0)
102	100, 101	eleqtri 2699	. . . . . . . . . . . . 13 ⊢ 0 ∈ (ℤ_≥‘0)
103	102	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑋 ∈ ℂ → 0 ∈ (ℤ_≥‘0))
104		3nn 11186	. . . . . . . . . . . . . . . . 17 ⊢ 3 ∈ ℕ
105		nnuz 11723	. . . . . . . . . . . . . . . . 17 ⊢ ℕ = (ℤ_≥‘1)
106	104, 105	eleqtri 2699	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ (ℤ_≥‘1)
107		fzss2 12381	. . . . . . . . . . . . . . . 16 ⊢ (3 ∈ (ℤ_≥‘1) → (0...1) ⊆ (0...3))
108	106, 107	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (0...1) ⊆ (0...3)
109		2p1e3 11151	. . . . . . . . . . . . . . . 16 ⊢ (2 + 1) = 3
110	109	oveq2i 6661	. . . . . . . . . . . . . . 15 ⊢ (0...(2 + 1)) = (0...3)
111	108, 98, 110	3sstr4i 3644	. . . . . . . . . . . . . 14 ⊢ (0...(0 + 1)) ⊆ (0...(2 + 1))
112	111	sseli 3599	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (0...(0 + 1)) → 𝑘 ∈ (0...(2 + 1)))
113	112, 49	sylan2 491	. . . . . . . . . . . 12 ⊢ ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(0 + 1))) → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) ∈ ℂ)
114	97	eqeq2i 2634	. . . . . . . . . . . . 13 ⊢ (𝑘 = (0 + 1) ↔ 𝑘 = 1)
115		oveq2 6658	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 1 → (4C𝑘) = (4C1))
116		bcn1 13100	. . . . . . . . . . . . . . . 16 ⊢ (4 ∈ ℕ₀ → (4C1) = 4)
117	1, 116	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (4C1) = 4
118	115, 117	syl6eq 2672	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 1 → (4C𝑘) = 4)
119		oveq1 6657	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 1 → (𝑘 BernPoly 𝑋) = (1 BernPoly 𝑋))
120		oveq2 6658	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 1 → (4 − 𝑘) = (4 − 1))
121	120	oveq1d 6665	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 1 → ((4 − 𝑘) + 1) = ((4 − 1) + 1))
122	4	oveq1i 6660	. . . . . . . . . . . . . . . . 17 ⊢ ((4 − 1) + 1) = (3 + 1)
123		df-4 11081	. . . . . . . . . . . . . . . . 17 ⊢ 4 = (3 + 1)
124	122, 123	eqtr4i 2647	. . . . . . . . . . . . . . . 16 ⊢ ((4 − 1) + 1) = 4
125	121, 124	syl6eq 2672	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 1 → ((4 − 𝑘) + 1) = 4)
126	119, 125	oveq12d 6668	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 1 → ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)) = ((1 BernPoly 𝑋) / 4))
127	118, 126	oveq12d 6668	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1 → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (4 · ((1 BernPoly 𝑋) / 4)))
128	114, 127	sylbi 207	. . . . . . . . . . . 12 ⊢ (𝑘 = (0 + 1) → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (4 · ((1 BernPoly 𝑋) / 4)))
129	103, 113, 128	fsump1 14487	. . . . . . . . . . 11 ⊢ (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...(0 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (Σ𝑘 ∈ (0...0)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) + (4 · ((1 BernPoly 𝑋) / 4))))
130		0z 11388	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℤ
131	59	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑋 ∈ ℂ → 1 ∈ ℂ)
132		bpolycl 14783	. . . . . . . . . . . . . . . . 17 ⊢ ((0 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → (0 BernPoly 𝑋) ∈ ℂ)
133	100, 132	mpan 706	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∈ ℂ → (0 BernPoly 𝑋) ∈ ℂ)
134		5cn 11100	. . . . . . . . . . . . . . . . 17 ⊢ 5 ∈ ℂ
135	134	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∈ ℂ → 5 ∈ ℂ)
136		0re 10040	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℝ
137		5pos 11118	. . . . . . . . . . . . . . . . . 18 ⊢ 0 < 5
138	136, 137	gtneii 10149	. . . . . . . . . . . . . . . . 17 ⊢ 5 ≠ 0
139	138	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∈ ℂ → 5 ≠ 0)
140	133, 135, 139	divcld 10801	. . . . . . . . . . . . . . 15 ⊢ (𝑋 ∈ ℂ → ((0 BernPoly 𝑋) / 5) ∈ ℂ)
141	131, 140	mulcld 10060	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ ℂ → (1 · ((0 BernPoly 𝑋) / 5)) ∈ ℂ)
142		oveq2 6658	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 0 → (4C𝑘) = (4C0))
143		bcn0 13097	. . . . . . . . . . . . . . . . . 18 ⊢ (4 ∈ ℕ₀ → (4C0) = 1)
144	1, 143	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (4C0) = 1
145	142, 144	syl6eq 2672	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 0 → (4C𝑘) = 1)
146		oveq1 6657	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 0 → (𝑘 BernPoly 𝑋) = (0 BernPoly 𝑋))
147		oveq2 6658	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 0 → (4 − 𝑘) = (4 − 0))
148	147	oveq1d 6665	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 0 → ((4 − 𝑘) + 1) = ((4 − 0) + 1))
149	57	subid1i 10353	. . . . . . . . . . . . . . . . . . . 20 ⊢ (4 − 0) = 4
150	149	oveq1i 6660	. . . . . . . . . . . . . . . . . . 19 ⊢ ((4 − 0) + 1) = (4 + 1)
151		4p1e5 11154	. . . . . . . . . . . . . . . . . . 19 ⊢ (4 + 1) = 5
152	150, 151	eqtri 2644	. . . . . . . . . . . . . . . . . 18 ⊢ ((4 − 0) + 1) = 5
153	148, 152	syl6eq 2672	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 0 → ((4 − 𝑘) + 1) = 5)
154	146, 153	oveq12d 6668	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 0 → ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)) = ((0 BernPoly 𝑋) / 5))
155	145, 154	oveq12d 6668	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 0 → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (1 · ((0 BernPoly 𝑋) / 5)))
156	155	fsum1 14476	. . . . . . . . . . . . . 14 ⊢ ((0 ∈ ℤ ∧ (1 · ((0 BernPoly 𝑋) / 5)) ∈ ℂ) → Σ𝑘 ∈ (0...0)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (1 · ((0 BernPoly 𝑋) / 5)))
157	130, 141, 156	sylancr 695	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...0)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (1 · ((0 BernPoly 𝑋) / 5)))
158		bpoly0 14781	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∈ ℂ → (0 BernPoly 𝑋) = 1)
159	158	oveq1d 6665	. . . . . . . . . . . . . . 15 ⊢ (𝑋 ∈ ℂ → ((0 BernPoly 𝑋) / 5) = (1 / 5))
160	159	oveq2d 6666	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ ℂ → (1 · ((0 BernPoly 𝑋) / 5)) = (1 · (1 / 5)))
161	134, 138	reccli 10755	. . . . . . . . . . . . . . 15 ⊢ (1 / 5) ∈ ℂ
162	161	mulid2i 10043	. . . . . . . . . . . . . 14 ⊢ (1 · (1 / 5)) = (1 / 5)
163	160, 162	syl6eq 2672	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ ℂ → (1 · ((0 BernPoly 𝑋) / 5)) = (1 / 5))
164	157, 163	eqtrd 2656	. . . . . . . . . . . 12 ⊢ (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...0)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (1 / 5))
165		1nn0 11308	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℕ₀
166		bpolycl 14783	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → (1 BernPoly 𝑋) ∈ ℂ)
167	165, 166	mpan 706	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ ℂ → (1 BernPoly 𝑋) ∈ ℂ)
168		nn0cn 11302	. . . . . . . . . . . . . . 15 ⊢ (4 ∈ ℕ₀ → 4 ∈ ℂ)
169	1, 168	mp1i 13	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ ℂ → 4 ∈ ℂ)
170		4ne0 11117	. . . . . . . . . . . . . . 15 ⊢ 4 ≠ 0
171	170	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ ℂ → 4 ≠ 0)
172	167, 169, 171	divcan2d 10803	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ ℂ → (4 · ((1 BernPoly 𝑋) / 4)) = (1 BernPoly 𝑋))
173		bpoly1 14782	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ ℂ → (1 BernPoly 𝑋) = (𝑋 − (1 / 2)))
174	172, 173	eqtrd 2656	. . . . . . . . . . . 12 ⊢ (𝑋 ∈ ℂ → (4 · ((1 BernPoly 𝑋) / 4)) = (𝑋 − (1 / 2)))
175	164, 174	oveq12d 6668	. . . . . . . . . . 11 ⊢ (𝑋 ∈ ℂ → (Σ𝑘 ∈ (0...0)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) + (4 · ((1 BernPoly 𝑋) / 4))) = ((1 / 5) + (𝑋 − (1 / 2))))
176	129, 175	eqtrd 2656	. . . . . . . . . 10 ⊢ (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...(0 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = ((1 / 5) + (𝑋 − (1 / 2))))
177	99, 176	syl5eqr 2670	. . . . . . . . 9 ⊢ (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...1)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = ((1 / 5) + (𝑋 − (1 / 2))))
178		6cn 11102	. . . . . . . . . . . 12 ⊢ 6 ∈ ℂ
179	178	a1i 11	. . . . . . . . . . 11 ⊢ (𝑋 ∈ ℂ → 6 ∈ ℂ)
180		2nn0 11309	. . . . . . . . . . . 12 ⊢ 2 ∈ ℕ₀
181		bpolycl 14783	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → (2 BernPoly 𝑋) ∈ ℂ)
182	180, 181	mpan 706	. . . . . . . . . . 11 ⊢ (𝑋 ∈ ℂ → (2 BernPoly 𝑋) ∈ ℂ)
183	58	a1i 11	. . . . . . . . . . 11 ⊢ (𝑋 ∈ ℂ → 3 ∈ ℂ)
184		3ne0 11115	. . . . . . . . . . . 12 ⊢ 3 ≠ 0
185	184	a1i 11	. . . . . . . . . . 11 ⊢ (𝑋 ∈ ℂ → 3 ≠ 0)
186	179, 182, 183, 185	div12d 10837	. . . . . . . . . 10 ⊢ (𝑋 ∈ ℂ → (6 · ((2 BernPoly 𝑋) / 3)) = ((2 BernPoly 𝑋) · (6 / 3)))
187		3t2e6 11179	. . . . . . . . . . . . 13 ⊢ (3 · 2) = 6
188	178, 58, 87, 184	divmuli 10779	. . . . . . . . . . . . 13 ⊢ ((6 / 3) = 2 ↔ (3 · 2) = 6)
189	187, 188	mpbir 221	. . . . . . . . . . . 12 ⊢ (6 / 3) = 2
190	189	oveq2i 6661	. . . . . . . . . . 11 ⊢ ((2 BernPoly 𝑋) · (6 / 3)) = ((2 BernPoly 𝑋) · 2)
191	87	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ ℂ → 2 ∈ ℂ)
192	182, 191	mulcomd 10061	. . . . . . . . . . . 12 ⊢ (𝑋 ∈ ℂ → ((2 BernPoly 𝑋) · 2) = (2 · (2 BernPoly 𝑋)))
193		bpoly2 14788	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ ℂ → (2 BernPoly 𝑋) = (((𝑋↑2) − 𝑋) + (1 / 6)))
194	193	oveq2d 6666	. . . . . . . . . . . 12 ⊢ (𝑋 ∈ ℂ → (2 · (2 BernPoly 𝑋)) = (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))
195	192, 194	eqtrd 2656	. . . . . . . . . . 11 ⊢ (𝑋 ∈ ℂ → ((2 BernPoly 𝑋) · 2) = (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))
196	190, 195	syl5eq 2668	. . . . . . . . . 10 ⊢ (𝑋 ∈ ℂ → ((2 BernPoly 𝑋) · (6 / 3)) = (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))
197	186, 196	eqtrd 2656	. . . . . . . . 9 ⊢ (𝑋 ∈ ℂ → (6 · ((2 BernPoly 𝑋) / 3)) = (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))
198	177, 197	oveq12d 6668	. . . . . . . 8 ⊢ (𝑋 ∈ ℂ → (Σ𝑘 ∈ (0...1)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) + (6 · ((2 BernPoly 𝑋) / 3))) = (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))))
199	96, 198	eqtrd 2656	. . . . . . 7 ⊢ (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...(1 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))))
200	71, 199	syl5eq 2668	. . . . . 6 ⊢ (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...2)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))))
201		3nn0 11310	. . . . . . . . 9 ⊢ 3 ∈ ℕ₀
202		bpolycl 14783	. . . . . . . . 9 ⊢ ((3 ∈ ℕ₀ ∧ 𝑋 ∈ ℂ) → (3 BernPoly 𝑋) ∈ ℂ)
203	201, 202	mpan 706	. . . . . . . 8 ⊢ (𝑋 ∈ ℂ → (3 BernPoly 𝑋) ∈ ℂ)
204		2ne0 11113	. . . . . . . . 9 ⊢ 2 ≠ 0
205	204	a1i 11	. . . . . . . 8 ⊢ (𝑋 ∈ ℂ → 2 ≠ 0)
206	169, 203, 191, 205	div12d 10837	. . . . . . 7 ⊢ (𝑋 ∈ ℂ → (4 · ((3 BernPoly 𝑋) / 2)) = ((3 BernPoly 𝑋) · (4 / 2)))
207		4d2e2 11184	. . . . . . . . 9 ⊢ (4 / 2) = 2
208	207	oveq2i 6661	. . . . . . . 8 ⊢ ((3 BernPoly 𝑋) · (4 / 2)) = ((3 BernPoly 𝑋) · 2)
209	203, 191	mulcomd 10061	. . . . . . . . 9 ⊢ (𝑋 ∈ ℂ → ((3 BernPoly 𝑋) · 2) = (2 · (3 BernPoly 𝑋)))
210		bpoly3 14789	. . . . . . . . . 10 ⊢ (𝑋 ∈ ℂ → (3 BernPoly 𝑋) = (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋)))
211	210	oveq2d 6666	. . . . . . . . 9 ⊢ (𝑋 ∈ ℂ → (2 · (3 BernPoly 𝑋)) = (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))))
212	209, 211	eqtrd 2656	. . . . . . . 8 ⊢ (𝑋 ∈ ℂ → ((3 BernPoly 𝑋) · 2) = (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))))
213	208, 212	syl5eq 2668	. . . . . . 7 ⊢ (𝑋 ∈ ℂ → ((3 BernPoly 𝑋) · (4 / 2)) = (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))))
214	206, 213	eqtrd 2656	. . . . . 6 ⊢ (𝑋 ∈ ℂ → (4 · ((3 BernPoly 𝑋) / 2)) = (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))))
215	200, 214	oveq12d 6668	. . . . 5 ⊢ (𝑋 ∈ ℂ → (Σ𝑘 ∈ (0...2)((4C𝑘) · ((𝑘 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 2656	. . . 4 ⊢ (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...(2 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = ((((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))) + (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋)))))
217	8, 216	syl5eq 2668	. . 3 ⊢ (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...(4 − 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = ((((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))) + (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋)))))
218	217	oveq2d 6666	. 2 ⊢ (𝑋 ∈ ℂ → ((𝑋↑4) − Σ𝑘 ∈ (0...(4 − 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)))) = ((𝑋↑4) − ((((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))) + (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))))))
219		expcl 12878	. . . . 5 ⊢ ((𝑋 ∈ ℂ ∧ 4 ∈ ℕ₀) → (𝑋↑4) ∈ ℂ)
220	1, 219	mpan2 707	. . . 4 ⊢ (𝑋 ∈ ℂ → (𝑋↑4) ∈ ℂ)
221		expcl 12878	. . . . . 6 ⊢ ((𝑋 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝑋↑3) ∈ ℂ)
222	201, 221	mpan2 707	. . . . 5 ⊢ (𝑋 ∈ ℂ → (𝑋↑3) ∈ ℂ)
223	191, 222	mulcld 10060	. . . 4 ⊢ (𝑋 ∈ ℂ → (2 · (𝑋↑3)) ∈ ℂ)
224		sqcl 12925	. . . . 5 ⊢ (𝑋 ∈ ℂ → (𝑋↑2) ∈ ℂ)
225	201, 100	deccl 11512	. . . . . . . 8 ⊢ ;30 ∈ ℕ₀
226	225	nn0cni 11304	. . . . . . 7 ⊢ ;30 ∈ ℂ
227		dfdec10 11497	. . . . . . . . 9 ⊢ ;30 = ((;10 · 3) + 0)
228		10re 11517	. . . . . . . . . . . 12 ⊢ ;10 ∈ ℝ
229	228	recni 10052	. . . . . . . . . . 11 ⊢ ;10 ∈ ℂ
230	229, 58	mulcli 10045	. . . . . . . . . 10 ⊢ (;10 · 3) ∈ ℂ
231	230	addid1i 10223	. . . . . . . . 9 ⊢ ((;10 · 3) + 0) = (;10 · 3)
232	227, 231	eqtri 2644	. . . . . . . 8 ⊢ ;30 = (;10 · 3)
233		10pos 11515	. . . . . . . . . 10 ⊢ 0 < ;10
234	136, 233	gtneii 10149	. . . . . . . . 9 ⊢ ;10 ≠ 0
235	229, 58, 234, 184	mulne0i 10670	. . . . . . . 8 ⊢ (;10 · 3) ≠ 0
236	232, 235	eqnetri 2864	. . . . . . 7 ⊢ ;30 ≠ 0
237	226, 236	reccli 10755	. . . . . 6 ⊢ (1 / ;30) ∈ ℂ
238	237	a1i 11	. . . . 5 ⊢ (𝑋 ∈ ℂ → (1 / ;30) ∈ ℂ)
239	224, 238	subcld 10392	. . . 4 ⊢ (𝑋 ∈ ℂ → ((𝑋↑2) − (1 / ;30)) ∈ ℂ)
240	220, 223, 239	subsubd 10420	. . 3 ⊢ (𝑋 ∈ ℂ → ((𝑋↑4) − ((2 · (𝑋↑3)) − ((𝑋↑2) − (1 / ;30)))) = (((𝑋↑4) − (2 · (𝑋↑3))) + ((𝑋↑2) − (1 / ;30))))
241	161	a1i 11	. . . . . . . 8 ⊢ (𝑋 ∈ ℂ → (1 / 5) ∈ ℂ)
242		id 22	. . . . . . . . 9 ⊢ (𝑋 ∈ ℂ → 𝑋 ∈ ℂ)
243	87, 204	reccli 10755	. . . . . . . . . 10 ⊢ (1 / 2) ∈ ℂ
244	243	a1i 11	. . . . . . . . 9 ⊢ (𝑋 ∈ ℂ → (1 / 2) ∈ ℂ)
245	242, 244	subcld 10392	. . . . . . . 8 ⊢ (𝑋 ∈ ℂ → (𝑋 − (1 / 2)) ∈ ℂ)
246	241, 245	addcld 10059	. . . . . . 7 ⊢ (𝑋 ∈ ℂ → ((1 / 5) + (𝑋 − (1 / 2))) ∈ ℂ)
247	224, 242	subcld 10392	. . . . . . . . 9 ⊢ (𝑋 ∈ ℂ → ((𝑋↑2) − 𝑋) ∈ ℂ)
248		6pos 11119	. . . . . . . . . . . 12 ⊢ 0 < 6
249	136, 248	gtneii 10149	. . . . . . . . . . 11 ⊢ 6 ≠ 0
250	178, 249	reccli 10755	. . . . . . . . . 10 ⊢ (1 / 6) ∈ ℂ
251	250	a1i 11	. . . . . . . . 9 ⊢ (𝑋 ∈ ℂ → (1 / 6) ∈ ℂ)
252	247, 251	addcld 10059	. . . . . . . 8 ⊢ (𝑋 ∈ ℂ → (((𝑋↑2) − 𝑋) + (1 / 6)) ∈ ℂ)
253	191, 252	mulcld 10060	. . . . . . 7 ⊢ (𝑋 ∈ ℂ → (2 · (((𝑋↑2) − 𝑋) + (1 / 6))) ∈ ℂ)
254	246, 253	addcld 10059	. . . . . 6 ⊢ (𝑋 ∈ ℂ → (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))) ∈ ℂ)
255	58, 87, 204	divcli 10767	. . . . . . . . . . 11 ⊢ (3 / 2) ∈ ℂ
256	255	a1i 11	. . . . . . . . . 10 ⊢ (𝑋 ∈ ℂ → (3 / 2) ∈ ℂ)
257	256, 224	mulcld 10060	. . . . . . . . 9 ⊢ (𝑋 ∈ ℂ → ((3 / 2) · (𝑋↑2)) ∈ ℂ)
258	222, 257	subcld 10392	. . . . . . . 8 ⊢ (𝑋 ∈ ℂ → ((𝑋↑3) − ((3 / 2) · (𝑋↑2))) ∈ ℂ)
259	244, 242	mulcld 10060	. . . . . . . 8 ⊢ (𝑋 ∈ ℂ → ((1 / 2) · 𝑋) ∈ ℂ)
260	258, 259	addcld 10059	. . . . . . 7 ⊢ (𝑋 ∈ ℂ → (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋)) ∈ ℂ)
261	191, 260	mulcld 10060	. . . . . 6 ⊢ (𝑋 ∈ ℂ → (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))) ∈ ℂ)
262	254, 261	addcomd 10238	. . . . 5 ⊢ (𝑋 ∈ ℂ → ((((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 10064	. . . . . . 7 ⊢ (𝑋 ∈ ℂ → (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))) = ((2 · ((𝑋↑3) − ((3 / 2) · (𝑋↑2)))) + (2 · ((1 / 2) · 𝑋))))
264	191, 222, 257	subdid 10486	. . . . . . . 8 ⊢ (𝑋 ∈ ℂ → (2 · ((𝑋↑3) − ((3 / 2) · (𝑋↑2)))) = ((2 · (𝑋↑3)) − (2 · ((3 / 2) · (𝑋↑2)))))
265	87, 204	recidi 10756	. . . . . . . . . 10 ⊢ (2 · (1 / 2)) = 1
266	265	oveq1i 6660	. . . . . . . . 9 ⊢ ((2 · (1 / 2)) · 𝑋) = (1 · 𝑋)
267	191, 244, 242	mulassd 10063	. . . . . . . . 9 ⊢ (𝑋 ∈ ℂ → ((2 · (1 / 2)) · 𝑋) = (2 · ((1 / 2) · 𝑋)))
268		mulid2 10038	. . . . . . . . 9 ⊢ (𝑋 ∈ ℂ → (1 · 𝑋) = 𝑋)
269	266, 267, 268	3eqtr3a 2680	. . . . . . . 8 ⊢ (𝑋 ∈ ℂ → (2 · ((1 / 2) · 𝑋)) = 𝑋)
270	264, 269	oveq12d 6668	. . . . . . 7 ⊢ (𝑋 ∈ ℂ → ((2 · ((𝑋↑3) − ((3 / 2) · (𝑋↑2)))) + (2 · ((1 / 2) · 𝑋))) = (((2 · (𝑋↑3)) − (2 · ((3 / 2) · (𝑋↑2)))) + 𝑋))
271	263, 270	eqtrd 2656	. . . . . 6 ⊢ (𝑋 ∈ ℂ → (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))) = (((2 · (𝑋↑3)) − (2 · ((3 / 2) · (𝑋↑2)))) + 𝑋))
272	271	oveq1d 6665	. . . . 5 ⊢ (𝑋 ∈ ℂ → ((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 10060	. . . . . . . 8 ⊢ (𝑋 ∈ ℂ → (2 · ((3 / 2) · (𝑋↑2))) ∈ ℂ)
274	223, 273	subcld 10392	. . . . . . 7 ⊢ (𝑋 ∈ ℂ → ((2 · (𝑋↑3)) − (2 · ((3 / 2) · (𝑋↑2)))) ∈ ℂ)
275	274, 242, 254	addassd 10062	. . . . . 6 ⊢ (𝑋 ∈ ℂ → ((((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 10059	. . . . . . 7 ⊢ (𝑋 ∈ ℂ → (𝑋 + (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))) ∈ ℂ)
277	223, 273, 276	subsubd 10420	. . . . . 6 ⊢ (𝑋 ∈ ℂ → ((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	58, 87, 204	divcan2i 10768	. . . . . . . . . . 11 ⊢ (2 · (3 / 2)) = 3
279	278	oveq1i 6660	. . . . . . . . . 10 ⊢ ((2 · (3 / 2)) · (𝑋↑2)) = (3 · (𝑋↑2))
280	191, 256, 224	mulassd 10063	. . . . . . . . . 10 ⊢ (𝑋 ∈ ℂ → ((2 · (3 / 2)) · (𝑋↑2)) = (2 · ((3 / 2) · (𝑋↑2))))
281	279, 280	syl5reqr 2671	. . . . . . . . 9 ⊢ (𝑋 ∈ ℂ → (2 · ((3 / 2) · (𝑋↑2))) = (3 · (𝑋↑2)))
282	281	oveq1d 6665	. . . . . . . 8 ⊢ (𝑋 ∈ ℂ → ((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 10262	. . . . . . . . . 10 ⊢ (𝑋 ∈ ℂ → (𝑋 + (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))) = (((1 / 5) + (𝑋 − (1 / 2))) + (𝑋 + (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))))
284	191, 247, 251	adddid 10064	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ ℂ → (2 · (((𝑋↑2) − 𝑋) + (1 / 6))) = ((2 · ((𝑋↑2) − 𝑋)) + (2 · (1 / 6))))
285	191, 224, 242	subdid 10486	. . . . . . . . . . . . . . 15 ⊢ (𝑋 ∈ ℂ → (2 · ((𝑋↑2) − 𝑋)) = ((2 · (𝑋↑2)) − (2 · 𝑋)))
286	187	oveq2i 6661	. . . . . . . . . . . . . . . . 17 ⊢ (2 / (3 · 2)) = (2 / 6)
287	58, 184	reccli 10755	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 / 3) ∈ ℂ
288	58, 87, 287	mul32i 10232	. . . . . . . . . . . . . . . . . . 19 ⊢ ((3 · 2) · (1 / 3)) = ((3 · (1 / 3)) · 2)
289	58, 184	recidi 10756	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (3 · (1 / 3)) = 1
290	289	oveq1i 6660	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((3 · (1 / 3)) · 2) = (1 · 2)
291	87	mulid2i 10043	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 · 2) = 2
292	290, 291	eqtri 2644	. . . . . . . . . . . . . . . . . . 19 ⊢ ((3 · (1 / 3)) · 2) = 2
293	288, 292	eqtri 2644	. . . . . . . . . . . . . . . . . 18 ⊢ ((3 · 2) · (1 / 3)) = 2
294	187, 178	eqeltri 2697	. . . . . . . . . . . . . . . . . . 19 ⊢ (3 · 2) ∈ ℂ
295	187, 249	eqnetri 2864	. . . . . . . . . . . . . . . . . . 19 ⊢ (3 · 2) ≠ 0
296	87, 294, 287, 295	divmuli 10779	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 / (3 · 2)) = (1 / 3) ↔ ((3 · 2) · (1 / 3)) = 2)
297	293, 296	mpbir 221	. . . . . . . . . . . . . . . . 17 ⊢ (2 / (3 · 2)) = (1 / 3)
298	87, 178, 249	divreci 10770	. . . . . . . . . . . . . . . . 17 ⊢ (2 / 6) = (2 · (1 / 6))
299	286, 297, 298	3eqtr3ri 2653	. . . . . . . . . . . . . . . 16 ⊢ (2 · (1 / 6)) = (1 / 3)
300	299	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑋 ∈ ℂ → (2 · (1 / 6)) = (1 / 3))
301	285, 300	oveq12d 6668	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ ℂ → ((2 · ((𝑋↑2) − 𝑋)) + (2 · (1 / 6))) = (((2 · (𝑋↑2)) − (2 · 𝑋)) + (1 / 3)))
302	284, 301	eqtrd 2656	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ ℂ → (2 · (((𝑋↑2) − 𝑋) + (1 / 6))) = (((2 · (𝑋↑2)) − (2 · 𝑋)) + (1 / 3)))
303	302	oveq2d 6666	. . . . . . . . . . . 12 ⊢ (𝑋 ∈ ℂ → (𝑋 + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))) = (𝑋 + (((2 · (𝑋↑2)) − (2 · 𝑋)) + (1 / 3))))
304	191, 224	mulcld 10060	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ ℂ → (2 · (𝑋↑2)) ∈ ℂ)
305	191, 242	mulcld 10060	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ ℂ → (2 · 𝑋) ∈ ℂ)
306	304, 305	subcld 10392	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ ℂ → ((2 · (𝑋↑2)) − (2 · 𝑋)) ∈ ℂ)
307	287	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ ℂ → (1 / 3) ∈ ℂ)
308	242, 306, 307	addassd 10062	. . . . . . . . . . . 12 ⊢ (𝑋 ∈ ℂ → ((𝑋 + ((2 · (𝑋↑2)) − (2 · 𝑋))) + (1 / 3)) = (𝑋 + (((2 · (𝑋↑2)) − (2 · 𝑋)) + (1 / 3))))
309	242, 304, 305	addsub12d 10415	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ ℂ → (𝑋 + ((2 · (𝑋↑2)) − (2 · 𝑋))) = ((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))))
310	309	oveq1d 6665	. . . . . . . . . . . 12 ⊢ (𝑋 ∈ ℂ → ((𝑋 + ((2 · (𝑋↑2)) − (2 · 𝑋))) + (1 / 3)) = (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3)))
311	303, 308, 310	3eqtr2d 2662	. . . . . . . . . . 11 ⊢ (𝑋 ∈ ℂ → (𝑋 + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))) = (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3)))
312	311	oveq2d 6666	. . . . . . . . . 10 ⊢ (𝑋 ∈ ℂ → (((1 / 5) + (𝑋 − (1 / 2))) + (𝑋 + (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))) = (((1 / 5) + (𝑋 − (1 / 2))) + (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3))))
313	283, 312	eqtrd 2656	. . . . . . . . 9 ⊢ (𝑋 ∈ ℂ → (𝑋 + (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))) = (((1 / 5) + (𝑋 − (1 / 2))) + (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3))))
314	313	oveq2d 6666	. . . . . . . 8 ⊢ (𝑋 ∈ ℂ → ((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 10392	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ ℂ → (𝑋 − (2 · 𝑋)) ∈ ℂ)
316	304, 315	addcld 10059	. . . . . . . . . . . 12 ⊢ (𝑋 ∈ ℂ → ((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) ∈ ℂ)
317	241, 245, 316, 307	add4d 10264	. . . . . . . . . . 11 ⊢ (𝑋 ∈ ℂ → (((1 / 5) + (𝑋 − (1 / 2))) + (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3))) = (((1 / 5) + ((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋)))) + ((𝑋 − (1 / 2)) + (1 / 3))))
318	241, 304, 315	add12d 10262	. . . . . . . . . . . 12 ⊢ (𝑋 ∈ ℂ → ((1 / 5) + ((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋)))) = ((2 · (𝑋↑2)) + ((1 / 5) + (𝑋 − (2 · 𝑋)))))
319	318	oveq1d 6665	. . . . . . . . . . 11 ⊢ (𝑋 ∈ ℂ → (((1 / 5) + ((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋)))) + ((𝑋 − (1 / 2)) + (1 / 3))) = (((2 · (𝑋↑2)) + ((1 / 5) + (𝑋 − (2 · 𝑋)))) + ((𝑋 − (1 / 2)) + (1 / 3))))
320	241, 315	addcld 10059	. . . . . . . . . . . 12 ⊢ (𝑋 ∈ ℂ → ((1 / 5) + (𝑋 − (2 · 𝑋))) ∈ ℂ)
321	245, 307	addcld 10059	. . . . . . . . . . . 12 ⊢ (𝑋 ∈ ℂ → ((𝑋 − (1 / 2)) + (1 / 3)) ∈ ℂ)
322	304, 320, 321	addassd 10062	. . . . . . . . . . 11 ⊢ (𝑋 ∈ ℂ → (((2 · (𝑋↑2)) + ((1 / 5) + (𝑋 − (2 · 𝑋)))) + ((𝑋 − (1 / 2)) + (1 / 3))) = ((2 · (𝑋↑2)) + (((1 / 5) + (𝑋 − (2 · 𝑋))) + ((𝑋 − (1 / 2)) + (1 / 3)))))
323	317, 319, 322	3eqtrd 2660	. . . . . . . . . 10 ⊢ (𝑋 ∈ ℂ → (((1 / 5) + (𝑋 − (1 / 2))) + (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3))) = ((2 · (𝑋↑2)) + (((1 / 5) + (𝑋 − (2 · 𝑋))) + ((𝑋 − (1 / 2)) + (1 / 3)))))
324	323	oveq2d 6666	. . . . . . . . 9 ⊢ (𝑋 ∈ ℂ → ((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 10060	. . . . . . . . . 10 ⊢ (𝑋 ∈ ℂ → (3 · (𝑋↑2)) ∈ ℂ)
326	320, 321	addcld 10059	. . . . . . . . . 10 ⊢ (𝑋 ∈ ℂ → (((1 / 5) + (𝑋 − (2 · 𝑋))) + ((𝑋 − (1 / 2)) + (1 / 3))) ∈ ℂ)
327	325, 304, 326	subsub4d 10423	. . . . . . . . 9 ⊢ (𝑋 ∈ ℂ → (((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 10370	. . . . . . . . . . . 12 ⊢ (3 − 2) = 1
329	328	oveq1i 6660	. . . . . . . . . . 11 ⊢ ((3 − 2) · (𝑋↑2)) = (1 · (𝑋↑2))
330	183, 191, 224	subdird 10487	. . . . . . . . . . 11 ⊢ (𝑋 ∈ ℂ → ((3 − 2) · (𝑋↑2)) = ((3 · (𝑋↑2)) − (2 · (𝑋↑2))))
331	224	mulid2d 10058	. . . . . . . . . . 11 ⊢ (𝑋 ∈ ℂ → (1 · (𝑋↑2)) = (𝑋↑2))
332	329, 330, 331	3eqtr3a 2680	. . . . . . . . . 10 ⊢ (𝑋 ∈ ℂ → ((3 · (𝑋↑2)) − (2 · (𝑋↑2))) = (𝑋↑2))
333	241, 305, 242	subsubd 10420	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ ℂ → ((1 / 5) − ((2 · 𝑋) − 𝑋)) = (((1 / 5) − (2 · 𝑋)) + 𝑋))
334		2txmxeqx 11149	. . . . . . . . . . . . . 14 ⊢ (𝑋 ∈ ℂ → ((2 · 𝑋) − 𝑋) = 𝑋)
335	334	oveq2d 6666	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ ℂ → ((1 / 5) − ((2 · 𝑋) − 𝑋)) = ((1 / 5) − 𝑋))
336	241, 305, 242	subadd23d 10414	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ ℂ → (((1 / 5) − (2 · 𝑋)) + 𝑋) = ((1 / 5) + (𝑋 − (2 · 𝑋))))
337	333, 335, 336	3eqtr3d 2664	. . . . . . . . . . . 12 ⊢ (𝑋 ∈ ℂ → ((1 / 5) − 𝑋) = ((1 / 5) + (𝑋 − (2 · 𝑋))))
338	242, 244, 307	subsubd 10420	. . . . . . . . . . . 12 ⊢ (𝑋 ∈ ℂ → (𝑋 − ((1 / 2) − (1 / 3))) = ((𝑋 − (1 / 2)) + (1 / 3)))
339	337, 338	oveq12d 6668	. . . . . . . . . . 11 ⊢ (𝑋 ∈ ℂ → (((1 / 5) − 𝑋) + (𝑋 − ((1 / 2) − (1 / 3)))) = (((1 / 5) + (𝑋 − (2 · 𝑋))) + ((𝑋 − (1 / 2)) + (1 / 3))))
340	243, 287	subcli 10357	. . . . . . . . . . . . . 14 ⊢ ((1 / 2) − (1 / 3)) ∈ ℂ
341	340	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑋 ∈ ℂ → ((1 / 2) − (1 / 3)) ∈ ℂ)
342	241, 242, 341	npncand 10416	. . . . . . . . . . . 12 ⊢ (𝑋 ∈ ℂ → (((1 / 5) − 𝑋) + (𝑋 − ((1 / 2) − (1 / 3)))) = ((1 / 5) − ((1 / 2) − (1 / 3))))
343		halfthird 11685	. . . . . . . . . . . . . 14 ⊢ ((1 / 2) − (1 / 3)) = (1 / 6)
344	343	oveq2i 6661	. . . . . . . . . . . . 13 ⊢ ((1 / 5) − ((1 / 2) − (1 / 3))) = ((1 / 5) − (1 / 6))
345		5recm6rec 11686	. . . . . . . . . . . . 13 ⊢ ((1 / 5) − (1 / 6)) = (1 / ;30)
346	344, 345	eqtri 2644	. . . . . . . . . . . 12 ⊢ ((1 / 5) − ((1 / 2) − (1 / 3))) = (1 / ;30)
347	342, 346	syl6eq 2672	. . . . . . . . . . 11 ⊢ (𝑋 ∈ ℂ → (((1 / 5) − 𝑋) + (𝑋 − ((1 / 2) − (1 / 3)))) = (1 / ;30))
348	339, 347	eqtr3d 2658	. . . . . . . . . 10 ⊢ (𝑋 ∈ ℂ → (((1 / 5) + (𝑋 − (2 · 𝑋))) + ((𝑋 − (1 / 2)) + (1 / 3))) = (1 / ;30))
349	332, 348	oveq12d 6668	. . . . . . . . 9 ⊢ (𝑋 ∈ ℂ → (((3 · (𝑋↑2)) − (2 · (𝑋↑2))) − (((1 / 5) + (𝑋 − (2 · 𝑋))) + ((𝑋 − (1 / 2)) + (1 / 3)))) = ((𝑋↑2) − (1 / ;30)))
350	324, 327, 349	3eqtr2d 2662	. . . . . . . 8 ⊢ (𝑋 ∈ ℂ → ((3 · (𝑋↑2)) − (((1 / 5) + (𝑋 − (1 / 2))) + (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3)))) = ((𝑋↑2) − (1 / ;30)))
351	282, 314, 350	3eqtrd 2660	. . . . . . 7 ⊢ (𝑋 ∈ ℂ → ((2 · ((3 / 2) · (𝑋↑2))) − (𝑋 + (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))))) = ((𝑋↑2) − (1 / ;30)))
352	351	oveq2d 6666	. . . . . 6 ⊢ (𝑋 ∈ ℂ → ((2 · (𝑋↑3)) − ((2 · ((3 / 2) · (𝑋↑2))) − (𝑋 + (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))))) = ((2 · (𝑋↑3)) − ((𝑋↑2) − (1 / ;30))))
353	275, 277, 352	3eqtr2d 2662	. . . . 5 ⊢ (𝑋 ∈ ℂ → ((((2 · (𝑋↑3)) − (2 · ((3 / 2) · (𝑋↑2)))) + 𝑋) + (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))) = ((2 · (𝑋↑3)) − ((𝑋↑2) − (1 / ;30))))
354	262, 272, 353	3eqtrd 2660	. . . 4 ⊢ (𝑋 ∈ ℂ → ((((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))) + (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋)))) = ((2 · (𝑋↑3)) − ((𝑋↑2) − (1 / ;30))))
355	354	oveq2d 6666	. . 3 ⊢ (𝑋 ∈ ℂ → ((𝑋↑4) − ((((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))) + (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))))) = ((𝑋↑4) − ((2 · (𝑋↑3)) − ((𝑋↑2) − (1 / ;30)))))
356	220, 223	subcld 10392	. . . 4 ⊢ (𝑋 ∈ ℂ → ((𝑋↑4) − (2 · (𝑋↑3))) ∈ ℂ)
357	356, 224, 238	addsubassd 10412	. . 3 ⊢ (𝑋 ∈ ℂ → ((((𝑋↑4) − (2 · (𝑋↑3))) + (𝑋↑2)) − (1 / ;30)) = (((𝑋↑4) − (2 · (𝑋↑3))) + ((𝑋↑2) − (1 / ;30))))
358	240, 355, 357	3eqtr4d 2666	. 2 ⊢ (𝑋 ∈ ℂ → ((𝑋↑4) − ((((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))) + (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))))) = ((((𝑋↑4) − (2 · (𝑋↑3))) + (𝑋↑2)) − (1 / ;30)))
359	3, 218, 358	3eqtrd 2660	1 ⊢ (𝑋 ∈ ℂ → (4 BernPoly 𝑋) = ((((𝑋↑4) − (2 · (𝑋↑3))) + (𝑋↑2)) − (1 / ;30)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 384 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ⊆ wss 3574 class class class wbr 4653 ‘cfv 5888 (class class class)co 6650 ℂcc 9934 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 · cmul 9941 < clt 10074 − cmin 10266 / cdiv 10684 ℕcn 11020 2c2 11070 3c3 11071 4c4 11072 5c5 11073 6c6 11074 ℕ₀cn0 11292 ℤcz 11377 cdc 11493 ℤ_≥cuz 11687 ...cfz 12326 ↑cexp 12860 Ccbc 13089 Σcsu 14416 BernPoly cbp 14777

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-sup 8348 df-oi 8415 df-card 8765 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-5 11082 df-6 11083 df-7 11084 df-8 11085 df-9 11086 df-n0 11293 df-z 11378 df-dec 11494 df-uz 11688 df-rp 11833 df-fz 12327 df-fzo 12466 df-seq 12802 df-exp 12861 df-fac 13061 df-bc 13090 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-clim 14219 df-sum 14417 df-bpoly 14778

This theorem is referenced by: fsumcube 14791

W3C validator