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

Theorem bpoly4 15942
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.
StepHypRef Expression
1 4nn0 12432 . . 3 4 ∈ ℕ0
2 bpolyval 15932 . . 3 ((4 ∈ ℕ0𝑋 ∈ ℂ) → (4 BernPoly 𝑋) = ((𝑋↑4) − Σ𝑘 ∈ (0...(4 − 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)))))
31, 2mpan 688 . 2 (𝑋 ∈ ℂ → (4 BernPoly 𝑋) = ((𝑋↑4) − Σ𝑘 ∈ (0...(4 − 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)))))
4 4m1e3 12282 . . . . . . 7 (4 − 1) = 3
5 df-3 12217 . . . . . . 7 3 = (2 + 1)
64, 5eqtri 2764 . . . . . 6 (4 − 1) = (2 + 1)
76oveq2i 7368 . . . . 5 (0...(4 − 1)) = (0...(2 + 1))
87sumeq1i 15583 . . . 4 Σ𝑘 ∈ (0...(4 − 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = Σ𝑘 ∈ (0...(2 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)))
9 2eluzge0 12818 . . . . . . 7 2 ∈ (ℤ‘0)
109a1i 11 . . . . . 6 (𝑋 ∈ ℂ → 2 ∈ (ℤ‘0))
11 elfzelz 13441 . . . . . . . . . 10 (𝑘 ∈ (0...(2 + 1)) → 𝑘 ∈ ℤ)
12 bccl 14222 . . . . . . . . . 10 ((4 ∈ ℕ0𝑘 ∈ ℤ) → (4C𝑘) ∈ ℕ0)
131, 11, 12sylancr 587 . . . . . . . . 9 (𝑘 ∈ (0...(2 + 1)) → (4C𝑘) ∈ ℕ0)
1413nn0cnd 12475 . . . . . . . 8 (𝑘 ∈ (0...(2 + 1)) → (4C𝑘) ∈ ℂ)
1514adantl 482 . . . . . . 7 ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(2 + 1))) → (4C𝑘) ∈ ℂ)
16 elfznn0 13534 . . . . . . . . . 10 (𝑘 ∈ (0...(2 + 1)) → 𝑘 ∈ ℕ0)
17 bpolycl 15935 . . . . . . . . . 10 ((𝑘 ∈ ℕ0𝑋 ∈ ℂ) → (𝑘 BernPoly 𝑋) ∈ ℂ)
1816, 17sylan 580 . . . . . . . . 9 ((𝑘 ∈ (0...(2 + 1)) ∧ 𝑋 ∈ ℂ) → (𝑘 BernPoly 𝑋) ∈ ℂ)
1918ancoms 459 . . . . . . . 8 ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(2 + 1))) → (𝑘 BernPoly 𝑋) ∈ ℂ)
20 4re 12237 . . . . . . . . . . . . 13 4 ∈ ℝ
2120a1i 11 . . . . . . . . . . . 12 (𝑘 ∈ (0...(2 + 1)) → 4 ∈ ℝ)
2211zred 12607 . . . . . . . . . . . 12 (𝑘 ∈ (0...(2 + 1)) → 𝑘 ∈ ℝ)
2321, 22resubcld 11583 . . . . . . . . . . 11 (𝑘 ∈ (0...(2 + 1)) → (4 − 𝑘) ∈ ℝ)
24 peano2re 11328 . . . . . . . . . . 11 ((4 − 𝑘) ∈ ℝ → ((4 − 𝑘) + 1) ∈ ℝ)
2523, 24syl 17 . . . . . . . . . 10 (𝑘 ∈ (0...(2 + 1)) → ((4 − 𝑘) + 1) ∈ ℝ)
2625recnd 11183 . . . . . . . . 9 (𝑘 ∈ (0...(2 + 1)) → ((4 − 𝑘) + 1) ∈ ℂ)
2726adantl 482 . . . . . . . 8 ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(2 + 1))) → ((4 − 𝑘) + 1) ∈ ℂ)
28 1red 11156 . . . . . . . . . . 11 (𝑘 ∈ (0...(2 + 1)) → 1 ∈ ℝ)
295oveq2i 7368 . . . . . . . . . . . . . 14 (0...3) = (0...(2 + 1))
3029eleq2i 2829 . . . . . . . . . . . . 13 (𝑘 ∈ (0...3) ↔ 𝑘 ∈ (0...(2 + 1)))
31 elfzelz 13441 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...3) → 𝑘 ∈ ℤ)
3231zred 12607 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...3) → 𝑘 ∈ ℝ)
33 3re 12233 . . . . . . . . . . . . . . 15 3 ∈ ℝ
3433a1i 11 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...3) → 3 ∈ ℝ)
3520a1i 11 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...3) → 4 ∈ ℝ)
36 elfzle2 13445 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...3) → 𝑘 ≤ 3)
37 3lt4 12327 . . . . . . . . . . . . . . 15 3 < 4
3837a1i 11 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...3) → 3 < 4)
3932, 34, 35, 36, 38lelttrd 11313 . . . . . . . . . . . . 13 (𝑘 ∈ (0...3) → 𝑘 < 4)
4030, 39sylbir 234 . . . . . . . . . . . 12 (𝑘 ∈ (0...(2 + 1)) → 𝑘 < 4)
4122, 21posdifd 11742 . . . . . . . . . . . 12 (𝑘 ∈ (0...(2 + 1)) → (𝑘 < 4 ↔ 0 < (4 − 𝑘)))
4240, 41mpbid 231 . . . . . . . . . . 11 (𝑘 ∈ (0...(2 + 1)) → 0 < (4 − 𝑘))
43 0lt1 11677 . . . . . . . . . . . 12 0 < 1
4443a1i 11 . . . . . . . . . . 11 (𝑘 ∈ (0...(2 + 1)) → 0 < 1)
4523, 28, 42, 44addgt0d 11730 . . . . . . . . . 10 (𝑘 ∈ (0...(2 + 1)) → 0 < ((4 − 𝑘) + 1))
4645gt0ne0d 11719 . . . . . . . . 9 (𝑘 ∈ (0...(2 + 1)) → ((4 − 𝑘) + 1) ≠ 0)
4746adantl 482 . . . . . . . 8 ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(2 + 1))) → ((4 − 𝑘) + 1) ≠ 0)
4819, 27, 47divcld 11931 . . . . . . 7 ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(2 + 1))) → ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)) ∈ ℂ)
4915, 48mulcld 11175 . . . . . 6 ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(2 + 1))) → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) ∈ ℂ)
505eqeq2i 2749 . . . . . . 7 (𝑘 = 3 ↔ 𝑘 = (2 + 1))
51 oveq2 7365 . . . . . . . . 9 (𝑘 = 3 → (4C𝑘) = (4C3))
52 4bc3eq4 14228 . . . . . . . . 9 (4C3) = 4
5351, 52eqtrdi 2792 . . . . . . . 8 (𝑘 = 3 → (4C𝑘) = 4)
54 oveq1 7364 . . . . . . . . 9 (𝑘 = 3 → (𝑘 BernPoly 𝑋) = (3 BernPoly 𝑋))
55 oveq2 7365 . . . . . . . . . . 11 (𝑘 = 3 → (4 − 𝑘) = (4 − 3))
5655oveq1d 7372 . . . . . . . . . 10 (𝑘 = 3 → ((4 − 𝑘) + 1) = ((4 − 3) + 1))
57 4cn 12238 . . . . . . . . . . . . 13 4 ∈ ℂ
58 3cn 12234 . . . . . . . . . . . . 13 3 ∈ ℂ
59 ax-1cn 11109 . . . . . . . . . . . . 13 1 ∈ ℂ
60 3p1e4 12298 . . . . . . . . . . . . 13 (3 + 1) = 4
6157, 58, 59, 60subaddrii 11490 . . . . . . . . . . . 12 (4 − 3) = 1
6261oveq1i 7367 . . . . . . . . . . 11 ((4 − 3) + 1) = (1 + 1)
63 df-2 12216 . . . . . . . . . . 11 2 = (1 + 1)
6462, 63eqtr4i 2767 . . . . . . . . . 10 ((4 − 3) + 1) = 2
6556, 64eqtrdi 2792 . . . . . . . . 9 (𝑘 = 3 → ((4 − 𝑘) + 1) = 2)
6654, 65oveq12d 7375 . . . . . . . 8 (𝑘 = 3 → ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)) = ((3 BernPoly 𝑋) / 2))
6753, 66oveq12d 7375 . . . . . . 7 (𝑘 = 3 → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (4 · ((3 BernPoly 𝑋) / 2)))
6850, 67sylbir 234 . . . . . 6 (𝑘 = (2 + 1) → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (4 · ((3 BernPoly 𝑋) / 2)))
6910, 49, 68fsump1 15641 . . . . 5 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...(2 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (Σ𝑘 ∈ (0...2)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) + (4 · ((3 BernPoly 𝑋) / 2))))
7063oveq2i 7368 . . . . . . . 8 (0...2) = (0...(1 + 1))
7170sumeq1i 15583 . . . . . . 7 Σ𝑘 ∈ (0...2)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = Σ𝑘 ∈ (0...(1 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)))
72 1eluzge0 12817 . . . . . . . . . 10 1 ∈ (ℤ‘0)
7372a1i 11 . . . . . . . . 9 (𝑋 ∈ ℂ → 1 ∈ (ℤ‘0))
74 fzssp1 13484 . . . . . . . . . . . 12 (0...(1 + 1)) ⊆ (0...((1 + 1) + 1))
7563oveq1i 7367 . . . . . . . . . . . . 13 (2 + 1) = ((1 + 1) + 1)
7675oveq2i 7368 . . . . . . . . . . . 12 (0...(2 + 1)) = (0...((1 + 1) + 1))
7774, 76sseqtrri 3981 . . . . . . . . . . 11 (0...(1 + 1)) ⊆ (0...(2 + 1))
7877sseli 3940 . . . . . . . . . 10 (𝑘 ∈ (0...(1 + 1)) → 𝑘 ∈ (0...(2 + 1)))
7978, 49sylan2 593 . . . . . . . . 9 ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(1 + 1))) → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) ∈ ℂ)
8063eqeq2i 2749 . . . . . . . . . 10 (𝑘 = 2 ↔ 𝑘 = (1 + 1))
81 oveq2 7365 . . . . . . . . . . . 12 (𝑘 = 2 → (4C𝑘) = (4C2))
82 4bc2eq6 14229 . . . . . . . . . . . 12 (4C2) = 6
8381, 82eqtrdi 2792 . . . . . . . . . . 11 (𝑘 = 2 → (4C𝑘) = 6)
84 oveq1 7364 . . . . . . . . . . . 12 (𝑘 = 2 → (𝑘 BernPoly 𝑋) = (2 BernPoly 𝑋))
85 oveq2 7365 . . . . . . . . . . . . . 14 (𝑘 = 2 → (4 − 𝑘) = (4 − 2))
8685oveq1d 7372 . . . . . . . . . . . . 13 (𝑘 = 2 → ((4 − 𝑘) + 1) = ((4 − 2) + 1))
87 2cn 12228 . . . . . . . . . . . . . . . 16 2 ∈ ℂ
88 2p2e4 12288 . . . . . . . . . . . . . . . 16 (2 + 2) = 4
8957, 87, 87, 88subaddrii 11490 . . . . . . . . . . . . . . 15 (4 − 2) = 2
9089oveq1i 7367 . . . . . . . . . . . . . 14 ((4 − 2) + 1) = (2 + 1)
9190, 5eqtr4i 2767 . . . . . . . . . . . . 13 ((4 − 2) + 1) = 3
9286, 91eqtrdi 2792 . . . . . . . . . . . 12 (𝑘 = 2 → ((4 − 𝑘) + 1) = 3)
9384, 92oveq12d 7375 . . . . . . . . . . 11 (𝑘 = 2 → ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)) = ((2 BernPoly 𝑋) / 3))
9483, 93oveq12d 7375 . . . . . . . . . 10 (𝑘 = 2 → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (6 · ((2 BernPoly 𝑋) / 3)))
9580, 94sylbir 234 . . . . . . . . 9 (𝑘 = (1 + 1) → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (6 · ((2 BernPoly 𝑋) / 3)))
9673, 79, 95fsump1 15641 . . . . . . . 8 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...(1 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (Σ𝑘 ∈ (0...1)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) + (6 · ((2 BernPoly 𝑋) / 3))))
97 0p1e1 12275 . . . . . . . . . . . 12 (0 + 1) = 1
9897oveq2i 7368 . . . . . . . . . . 11 (0...(0 + 1)) = (0...1)
9998sumeq1i 15583 . . . . . . . . . 10 Σ𝑘 ∈ (0...(0 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = Σ𝑘 ∈ (0...1)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)))
100 0nn0 12428 . . . . . . . . . . . . . 14 0 ∈ ℕ0
101 nn0uz 12805 . . . . . . . . . . . . . 14 0 = (ℤ‘0)
102100, 101eleqtri 2836 . . . . . . . . . . . . 13 0 ∈ (ℤ‘0)
103102a1i 11 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → 0 ∈ (ℤ‘0))
104 3nn 12232 . . . . . . . . . . . . . . . . 17 3 ∈ ℕ
105 nnuz 12806 . . . . . . . . . . . . . . . . 17 ℕ = (ℤ‘1)
106104, 105eleqtri 2836 . . . . . . . . . . . . . . . 16 3 ∈ (ℤ‘1)
107 fzss2 13481 . . . . . . . . . . . . . . . 16 (3 ∈ (ℤ‘1) → (0...1) ⊆ (0...3))
108106, 107ax-mp 5 . . . . . . . . . . . . . . 15 (0...1) ⊆ (0...3)
109 2p1e3 12295 . . . . . . . . . . . . . . . 16 (2 + 1) = 3
110109oveq2i 7368 . . . . . . . . . . . . . . 15 (0...(2 + 1)) = (0...3)
111108, 98, 1103sstr4i 3987 . . . . . . . . . . . . . 14 (0...(0 + 1)) ⊆ (0...(2 + 1))
112111sseli 3940 . . . . . . . . . . . . 13 (𝑘 ∈ (0...(0 + 1)) → 𝑘 ∈ (0...(2 + 1)))
113112, 49sylan2 593 . . . . . . . . . . . 12 ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(0 + 1))) → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) ∈ ℂ)
11497eqeq2i 2749 . . . . . . . . . . . . 13 (𝑘 = (0 + 1) ↔ 𝑘 = 1)
115 oveq2 7365 . . . . . . . . . . . . . . 15 (𝑘 = 1 → (4C𝑘) = (4C1))
116 bcn1 14213 . . . . . . . . . . . . . . . 16 (4 ∈ ℕ0 → (4C1) = 4)
1171, 116ax-mp 5 . . . . . . . . . . . . . . 15 (4C1) = 4
118115, 117eqtrdi 2792 . . . . . . . . . . . . . 14 (𝑘 = 1 → (4C𝑘) = 4)
119 oveq1 7364 . . . . . . . . . . . . . . 15 (𝑘 = 1 → (𝑘 BernPoly 𝑋) = (1 BernPoly 𝑋))
120 oveq2 7365 . . . . . . . . . . . . . . . . 17 (𝑘 = 1 → (4 − 𝑘) = (4 − 1))
121120oveq1d 7372 . . . . . . . . . . . . . . . 16 (𝑘 = 1 → ((4 − 𝑘) + 1) = ((4 − 1) + 1))
1224oveq1i 7367 . . . . . . . . . . . . . . . . 17 ((4 − 1) + 1) = (3 + 1)
123 df-4 12218 . . . . . . . . . . . . . . . . 17 4 = (3 + 1)
124122, 123eqtr4i 2767 . . . . . . . . . . . . . . . 16 ((4 − 1) + 1) = 4
125121, 124eqtrdi 2792 . . . . . . . . . . . . . . 15 (𝑘 = 1 → ((4 − 𝑘) + 1) = 4)
126119, 125oveq12d 7375 . . . . . . . . . . . . . 14 (𝑘 = 1 → ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)) = ((1 BernPoly 𝑋) / 4))
127118, 126oveq12d 7375 . . . . . . . . . . . . 13 (𝑘 = 1 → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (4 · ((1 BernPoly 𝑋) / 4)))
128114, 127sylbi 216 . . . . . . . . . . . 12 (𝑘 = (0 + 1) → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (4 · ((1 BernPoly 𝑋) / 4)))
129103, 113, 128fsump1 15641 . . . . . . . . . . 11 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...(0 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (Σ𝑘 ∈ (0...0)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) + (4 · ((1 BernPoly 𝑋) / 4))))
130 0z 12510 . . . . . . . . . . . . . 14 0 ∈ ℤ
13159a1i 11 . . . . . . . . . . . . . . 15 (𝑋 ∈ ℂ → 1 ∈ ℂ)
132 bpolycl 15935 . . . . . . . . . . . . . . . . 17 ((0 ∈ ℕ0𝑋 ∈ ℂ) → (0 BernPoly 𝑋) ∈ ℂ)
133100, 132mpan 688 . . . . . . . . . . . . . . . 16 (𝑋 ∈ ℂ → (0 BernPoly 𝑋) ∈ ℂ)
134 5cn 12241 . . . . . . . . . . . . . . . . 17 5 ∈ ℂ
135134a1i 11 . . . . . . . . . . . . . . . 16 (𝑋 ∈ ℂ → 5 ∈ ℂ)
136 0re 11157 . . . . . . . . . . . . . . . . . 18 0 ∈ ℝ
137 5pos 12262 . . . . . . . . . . . . . . . . . 18 0 < 5
138136, 137gtneii 11267 . . . . . . . . . . . . . . . . 17 5 ≠ 0
139138a1i 11 . . . . . . . . . . . . . . . 16 (𝑋 ∈ ℂ → 5 ≠ 0)
140133, 135, 139divcld 11931 . . . . . . . . . . . . . . 15 (𝑋 ∈ ℂ → ((0 BernPoly 𝑋) / 5) ∈ ℂ)
141131, 140mulcld 11175 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → (1 · ((0 BernPoly 𝑋) / 5)) ∈ ℂ)
142 oveq2 7365 . . . . . . . . . . . . . . . . 17 (𝑘 = 0 → (4C𝑘) = (4C0))
143 bcn0 14210 . . . . . . . . . . . . . . . . . 18 (4 ∈ ℕ0 → (4C0) = 1)
1441, 143ax-mp 5 . . . . . . . . . . . . . . . . 17 (4C0) = 1
145142, 144eqtrdi 2792 . . . . . . . . . . . . . . . 16 (𝑘 = 0 → (4C𝑘) = 1)
146 oveq1 7364 . . . . . . . . . . . . . . . . 17 (𝑘 = 0 → (𝑘 BernPoly 𝑋) = (0 BernPoly 𝑋))
147 oveq2 7365 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 0 → (4 − 𝑘) = (4 − 0))
148147oveq1d 7372 . . . . . . . . . . . . . . . . . 18 (𝑘 = 0 → ((4 − 𝑘) + 1) = ((4 − 0) + 1))
14957subid1i 11473 . . . . . . . . . . . . . . . . . . . 20 (4 − 0) = 4
150149oveq1i 7367 . . . . . . . . . . . . . . . . . . 19 ((4 − 0) + 1) = (4 + 1)
151 4p1e5 12299 . . . . . . . . . . . . . . . . . . 19 (4 + 1) = 5
152150, 151eqtri 2764 . . . . . . . . . . . . . . . . . 18 ((4 − 0) + 1) = 5
153148, 152eqtrdi 2792 . . . . . . . . . . . . . . . . 17 (𝑘 = 0 → ((4 − 𝑘) + 1) = 5)
154146, 153oveq12d 7375 . . . . . . . . . . . . . . . 16 (𝑘 = 0 → ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)) = ((0 BernPoly 𝑋) / 5))
155145, 154oveq12d 7375 . . . . . . . . . . . . . . 15 (𝑘 = 0 → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (1 · ((0 BernPoly 𝑋) / 5)))
156155fsum1 15632 . . . . . . . . . . . . . 14 ((0 ∈ ℤ ∧ (1 · ((0 BernPoly 𝑋) / 5)) ∈ ℂ) → Σ𝑘 ∈ (0...0)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (1 · ((0 BernPoly 𝑋) / 5)))
157130, 141, 156sylancr 587 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...0)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (1 · ((0 BernPoly 𝑋) / 5)))
158 bpoly0 15933 . . . . . . . . . . . . . . . 16 (𝑋 ∈ ℂ → (0 BernPoly 𝑋) = 1)
159158oveq1d 7372 . . . . . . . . . . . . . . 15 (𝑋 ∈ ℂ → ((0 BernPoly 𝑋) / 5) = (1 / 5))
160159oveq2d 7373 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → (1 · ((0 BernPoly 𝑋) / 5)) = (1 · (1 / 5)))
161134, 138reccli 11885 . . . . . . . . . . . . . . 15 (1 / 5) ∈ ℂ
162161mulid2i 11160 . . . . . . . . . . . . . 14 (1 · (1 / 5)) = (1 / 5)
163160, 162eqtrdi 2792 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (1 · ((0 BernPoly 𝑋) / 5)) = (1 / 5))
164157, 163eqtrd 2776 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...0)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (1 / 5))
165 1nn0 12429 . . . . . . . . . . . . . . 15 1 ∈ ℕ0
166 bpolycl 15935 . . . . . . . . . . . . . . 15 ((1 ∈ ℕ0𝑋 ∈ ℂ) → (1 BernPoly 𝑋) ∈ ℂ)
167165, 166mpan 688 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → (1 BernPoly 𝑋) ∈ ℂ)
168 nn0cn 12423 . . . . . . . . . . . . . . 15 (4 ∈ ℕ0 → 4 ∈ ℂ)
1691, 168mp1i 13 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → 4 ∈ ℂ)
170 4ne0 12261 . . . . . . . . . . . . . . 15 4 ≠ 0
171170a1i 11 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → 4 ≠ 0)
172167, 169, 171divcan2d 11933 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (4 · ((1 BernPoly 𝑋) / 4)) = (1 BernPoly 𝑋))
173 bpoly1 15934 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (1 BernPoly 𝑋) = (𝑋 − (1 / 2)))
174172, 173eqtrd 2776 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → (4 · ((1 BernPoly 𝑋) / 4)) = (𝑋 − (1 / 2)))
175164, 174oveq12d 7375 . . . . . . . . . . 11 (𝑋 ∈ ℂ → (Σ𝑘 ∈ (0...0)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) + (4 · ((1 BernPoly 𝑋) / 4))) = ((1 / 5) + (𝑋 − (1 / 2))))
176129, 175eqtrd 2776 . . . . . . . . . 10 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...(0 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = ((1 / 5) + (𝑋 − (1 / 2))))
17799, 176eqtr3id 2790 . . . . . . . . 9 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...1)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = ((1 / 5) + (𝑋 − (1 / 2))))
178 6cn 12244 . . . . . . . . . . . 12 6 ∈ ℂ
179178a1i 11 . . . . . . . . . . 11 (𝑋 ∈ ℂ → 6 ∈ ℂ)
180 2nn0 12430 . . . . . . . . . . . 12 2 ∈ ℕ0
181 bpolycl 15935 . . . . . . . . . . . 12 ((2 ∈ ℕ0𝑋 ∈ ℂ) → (2 BernPoly 𝑋) ∈ ℂ)
182180, 181mpan 688 . . . . . . . . . . 11 (𝑋 ∈ ℂ → (2 BernPoly 𝑋) ∈ ℂ)
18358a1i 11 . . . . . . . . . . 11 (𝑋 ∈ ℂ → 3 ∈ ℂ)
184 3ne0 12259 . . . . . . . . . . . 12 3 ≠ 0
185184a1i 11 . . . . . . . . . . 11 (𝑋 ∈ ℂ → 3 ≠ 0)
186179, 182, 183, 185div12d 11967 . . . . . . . . . 10 (𝑋 ∈ ℂ → (6 · ((2 BernPoly 𝑋) / 3)) = ((2 BernPoly 𝑋) · (6 / 3)))
187 3t2e6 12319 . . . . . . . . . . . . 13 (3 · 2) = 6
188178, 58, 87, 184divmuli 11909 . . . . . . . . . . . . 13 ((6 / 3) = 2 ↔ (3 · 2) = 6)
189187, 188mpbir 230 . . . . . . . . . . . 12 (6 / 3) = 2
190189oveq2i 7368 . . . . . . . . . . 11 ((2 BernPoly 𝑋) · (6 / 3)) = ((2 BernPoly 𝑋) · 2)
19187a1i 11 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → 2 ∈ ℂ)
192182, 191mulcomd 11176 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → ((2 BernPoly 𝑋) · 2) = (2 · (2 BernPoly 𝑋)))
193 bpoly2 15940 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (2 BernPoly 𝑋) = (((𝑋↑2) − 𝑋) + (1 / 6)))
194193oveq2d 7373 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → (2 · (2 BernPoly 𝑋)) = (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))
195192, 194eqtrd 2776 . . . . . . . . . . 11 (𝑋 ∈ ℂ → ((2 BernPoly 𝑋) · 2) = (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))
196190, 195eqtrid 2788 . . . . . . . . . 10 (𝑋 ∈ ℂ → ((2 BernPoly 𝑋) · (6 / 3)) = (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))
197186, 196eqtrd 2776 . . . . . . . . 9 (𝑋 ∈ ℂ → (6 · ((2 BernPoly 𝑋) / 3)) = (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))
198177, 197oveq12d 7375 . . . . . . . 8 (𝑋 ∈ ℂ → (Σ𝑘 ∈ (0...1)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) + (6 · ((2 BernPoly 𝑋) / 3))) = (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))))
19996, 198eqtrd 2776 . . . . . . 7 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...(1 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))))
20071, 199eqtrid 2788 . . . . . 6 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...2)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))))
201 3nn0 12431 . . . . . . . . 9 3 ∈ ℕ0
202 bpolycl 15935 . . . . . . . . 9 ((3 ∈ ℕ0𝑋 ∈ ℂ) → (3 BernPoly 𝑋) ∈ ℂ)
203201, 202mpan 688 . . . . . . . 8 (𝑋 ∈ ℂ → (3 BernPoly 𝑋) ∈ ℂ)
204 2ne0 12257 . . . . . . . . 9 2 ≠ 0
205204a1i 11 . . . . . . . 8 (𝑋 ∈ ℂ → 2 ≠ 0)
206169, 203, 191, 205div12d 11967 . . . . . . 7 (𝑋 ∈ ℂ → (4 · ((3 BernPoly 𝑋) / 2)) = ((3 BernPoly 𝑋) · (4 / 2)))
207 4d2e2 12323 . . . . . . . . 9 (4 / 2) = 2
208207oveq2i 7368 . . . . . . . 8 ((3 BernPoly 𝑋) · (4 / 2)) = ((3 BernPoly 𝑋) · 2)
209203, 191mulcomd 11176 . . . . . . . . 9 (𝑋 ∈ ℂ → ((3 BernPoly 𝑋) · 2) = (2 · (3 BernPoly 𝑋)))
210 bpoly3 15941 . . . . . . . . . 10 (𝑋 ∈ ℂ → (3 BernPoly 𝑋) = (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋)))
211210oveq2d 7373 . . . . . . . . 9 (𝑋 ∈ ℂ → (2 · (3 BernPoly 𝑋)) = (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))))
212209, 211eqtrd 2776 . . . . . . . 8 (𝑋 ∈ ℂ → ((3 BernPoly 𝑋) · 2) = (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))))
213208, 212eqtrid 2788 . . . . . . 7 (𝑋 ∈ ℂ → ((3 BernPoly 𝑋) · (4 / 2)) = (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))))
214206, 213eqtrd 2776 . . . . . 6 (𝑋 ∈ ℂ → (4 · ((3 BernPoly 𝑋) / 2)) = (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))))
215200, 214oveq12d 7375 . . . . 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) · 𝑋)))))
21669, 215eqtrd 2776 . . . 4 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...(2 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = ((((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))) + (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋)))))
2178, 216eqtrid 2788 . . 3 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...(4 − 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = ((((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))) + (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋)))))
218217oveq2d 7373 . 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 13985 . . . . 5 ((𝑋 ∈ ℂ ∧ 4 ∈ ℕ0) → (𝑋↑4) ∈ ℂ)
2201, 219mpan2 689 . . . 4 (𝑋 ∈ ℂ → (𝑋↑4) ∈ ℂ)
221 expcl 13985 . . . . . 6 ((𝑋 ∈ ℂ ∧ 3 ∈ ℕ0) → (𝑋↑3) ∈ ℂ)
222201, 221mpan2 689 . . . . 5 (𝑋 ∈ ℂ → (𝑋↑3) ∈ ℂ)
223191, 222mulcld 11175 . . . 4 (𝑋 ∈ ℂ → (2 · (𝑋↑3)) ∈ ℂ)
224 sqcl 14023 . . . . 5 (𝑋 ∈ ℂ → (𝑋↑2) ∈ ℂ)
225201, 100deccl 12633 . . . . . . . 8 30 ∈ ℕ0
226225nn0cni 12425 . . . . . . 7 30 ∈ ℂ
227 dfdec10 12621 . . . . . . . . 9 30 = ((10 · 3) + 0)
228 10re 12637 . . . . . . . . . . . 12 10 ∈ ℝ
229228recni 11169 . . . . . . . . . . 11 10 ∈ ℂ
230229, 58mulcli 11162 . . . . . . . . . 10 (10 · 3) ∈ ℂ
231230addid1i 11342 . . . . . . . . 9 ((10 · 3) + 0) = (10 · 3)
232227, 231eqtri 2764 . . . . . . . 8 30 = (10 · 3)
233 10pos 12635 . . . . . . . . . 10 0 < 10
234136, 233gtneii 11267 . . . . . . . . 9 10 ≠ 0
235229, 58, 234, 184mulne0i 11798 . . . . . . . 8 (10 · 3) ≠ 0
236232, 235eqnetri 3014 . . . . . . 7 30 ≠ 0
237226, 236reccli 11885 . . . . . 6 (1 / 30) ∈ ℂ
238237a1i 11 . . . . 5 (𝑋 ∈ ℂ → (1 / 30) ∈ ℂ)
239224, 238subcld 11512 . . . 4 (𝑋 ∈ ℂ → ((𝑋↑2) − (1 / 30)) ∈ ℂ)
240220, 223, 239subsubd 11540 . . 3 (𝑋 ∈ ℂ → ((𝑋↑4) − ((2 · (𝑋↑3)) − ((𝑋↑2) − (1 / 30)))) = (((𝑋↑4) − (2 · (𝑋↑3))) + ((𝑋↑2) − (1 / 30))))
241161a1i 11 . . . . . . . 8 (𝑋 ∈ ℂ → (1 / 5) ∈ ℂ)
242 id 22 . . . . . . . . 9 (𝑋 ∈ ℂ → 𝑋 ∈ ℂ)
24387, 204reccli 11885 . . . . . . . . . 10 (1 / 2) ∈ ℂ
244243a1i 11 . . . . . . . . 9 (𝑋 ∈ ℂ → (1 / 2) ∈ ℂ)
245242, 244subcld 11512 . . . . . . . 8 (𝑋 ∈ ℂ → (𝑋 − (1 / 2)) ∈ ℂ)
246241, 245addcld 11174 . . . . . . 7 (𝑋 ∈ ℂ → ((1 / 5) + (𝑋 − (1 / 2))) ∈ ℂ)
247224, 242subcld 11512 . . . . . . . . 9 (𝑋 ∈ ℂ → ((𝑋↑2) − 𝑋) ∈ ℂ)
248 6pos 12263 . . . . . . . . . . . 12 0 < 6
249136, 248gtneii 11267 . . . . . . . . . . 11 6 ≠ 0
250178, 249reccli 11885 . . . . . . . . . 10 (1 / 6) ∈ ℂ
251250a1i 11 . . . . . . . . 9 (𝑋 ∈ ℂ → (1 / 6) ∈ ℂ)
252247, 251addcld 11174 . . . . . . . 8 (𝑋 ∈ ℂ → (((𝑋↑2) − 𝑋) + (1 / 6)) ∈ ℂ)
253191, 252mulcld 11175 . . . . . . 7 (𝑋 ∈ ℂ → (2 · (((𝑋↑2) − 𝑋) + (1 / 6))) ∈ ℂ)
254246, 253addcld 11174 . . . . . 6 (𝑋 ∈ ℂ → (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))) ∈ ℂ)
25558, 87, 204divcli 11897 . . . . . . . . . . 11 (3 / 2) ∈ ℂ
256255a1i 11 . . . . . . . . . 10 (𝑋 ∈ ℂ → (3 / 2) ∈ ℂ)
257256, 224mulcld 11175 . . . . . . . . 9 (𝑋 ∈ ℂ → ((3 / 2) · (𝑋↑2)) ∈ ℂ)
258222, 257subcld 11512 . . . . . . . 8 (𝑋 ∈ ℂ → ((𝑋↑3) − ((3 / 2) · (𝑋↑2))) ∈ ℂ)
259244, 242mulcld 11175 . . . . . . . 8 (𝑋 ∈ ℂ → ((1 / 2) · 𝑋) ∈ ℂ)
260258, 259addcld 11174 . . . . . . 7 (𝑋 ∈ ℂ → (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋)) ∈ ℂ)
261191, 260mulcld 11175 . . . . . 6 (𝑋 ∈ ℂ → (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))) ∈ ℂ)
262254, 261addcomd 11357 . . . . 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))))))
263191, 258, 259adddid 11179 . . . . . . 7 (𝑋 ∈ ℂ → (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))) = ((2 · ((𝑋↑3) − ((3 / 2) · (𝑋↑2)))) + (2 · ((1 / 2) · 𝑋))))
264191, 222, 257subdid 11611 . . . . . . . 8 (𝑋 ∈ ℂ → (2 · ((𝑋↑3) − ((3 / 2) · (𝑋↑2)))) = ((2 · (𝑋↑3)) − (2 · ((3 / 2) · (𝑋↑2)))))
26587, 204recidi 11886 . . . . . . . . . 10 (2 · (1 / 2)) = 1
266265oveq1i 7367 . . . . . . . . 9 ((2 · (1 / 2)) · 𝑋) = (1 · 𝑋)
267191, 244, 242mulassd 11178 . . . . . . . . 9 (𝑋 ∈ ℂ → ((2 · (1 / 2)) · 𝑋) = (2 · ((1 / 2) · 𝑋)))
268 mulid2 11154 . . . . . . . . 9 (𝑋 ∈ ℂ → (1 · 𝑋) = 𝑋)
269266, 267, 2683eqtr3a 2800 . . . . . . . 8 (𝑋 ∈ ℂ → (2 · ((1 / 2) · 𝑋)) = 𝑋)
270264, 269oveq12d 7375 . . . . . . 7 (𝑋 ∈ ℂ → ((2 · ((𝑋↑3) − ((3 / 2) · (𝑋↑2)))) + (2 · ((1 / 2) · 𝑋))) = (((2 · (𝑋↑3)) − (2 · ((3 / 2) · (𝑋↑2)))) + 𝑋))
271263, 270eqtrd 2776 . . . . . 6 (𝑋 ∈ ℂ → (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))) = (((2 · (𝑋↑3)) − (2 · ((3 / 2) · (𝑋↑2)))) + 𝑋))
272271oveq1d 7372 . . . . 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))))))
273191, 257mulcld 11175 . . . . . . . 8 (𝑋 ∈ ℂ → (2 · ((3 / 2) · (𝑋↑2))) ∈ ℂ)
274223, 273subcld 11512 . . . . . . 7 (𝑋 ∈ ℂ → ((2 · (𝑋↑3)) − (2 · ((3 / 2) · (𝑋↑2)))) ∈ ℂ)
275274, 242, 254addassd 11177 . . . . . 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)))))))
276242, 254addcld 11174 . . . . . . 7 (𝑋 ∈ ℂ → (𝑋 + (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))) ∈ ℂ)
277223, 273, 276subsubd 11540 . . . . . 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)))))))
278191, 256, 224mulassd 11178 . . . . . . . . . 10 (𝑋 ∈ ℂ → ((2 · (3 / 2)) · (𝑋↑2)) = (2 · ((3 / 2) · (𝑋↑2))))
27958, 87, 204divcan2i 11898 . . . . . . . . . . 11 (2 · (3 / 2)) = 3
280279oveq1i 7367 . . . . . . . . . 10 ((2 · (3 / 2)) · (𝑋↑2)) = (3 · (𝑋↑2))
281278, 280eqtr3di 2791 . . . . . . . . 9 (𝑋 ∈ ℂ → (2 · ((3 / 2) · (𝑋↑2))) = (3 · (𝑋↑2)))
282281oveq1d 7372 . . . . . . . 8 (𝑋 ∈ ℂ → ((2 · ((3 / 2) · (𝑋↑2))) − (𝑋 + (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))))) = ((3 · (𝑋↑2)) − (𝑋 + (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))))))
283242, 246, 253add12d 11381 . . . . . . . . . 10 (𝑋 ∈ ℂ → (𝑋 + (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))) = (((1 / 5) + (𝑋 − (1 / 2))) + (𝑋 + (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))))
284191, 247, 251adddid 11179 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → (2 · (((𝑋↑2) − 𝑋) + (1 / 6))) = ((2 · ((𝑋↑2) − 𝑋)) + (2 · (1 / 6))))
285191, 224, 242subdid 11611 . . . . . . . . . . . . . . 15 (𝑋 ∈ ℂ → (2 · ((𝑋↑2) − 𝑋)) = ((2 · (𝑋↑2)) − (2 · 𝑋)))
286187oveq2i 7368 . . . . . . . . . . . . . . . . 17 (2 / (3 · 2)) = (2 / 6)
28758, 184reccli 11885 . . . . . . . . . . . . . . . . . . . 20 (1 / 3) ∈ ℂ
28858, 87, 287mul32i 11351 . . . . . . . . . . . . . . . . . . 19 ((3 · 2) · (1 / 3)) = ((3 · (1 / 3)) · 2)
28958, 184recidi 11886 . . . . . . . . . . . . . . . . . . . . 21 (3 · (1 / 3)) = 1
290289oveq1i 7367 . . . . . . . . . . . . . . . . . . . 20 ((3 · (1 / 3)) · 2) = (1 · 2)
29187mulid2i 11160 . . . . . . . . . . . . . . . . . . . 20 (1 · 2) = 2
292290, 291eqtri 2764 . . . . . . . . . . . . . . . . . . 19 ((3 · (1 / 3)) · 2) = 2
293288, 292eqtri 2764 . . . . . . . . . . . . . . . . . 18 ((3 · 2) · (1 / 3)) = 2
294187, 178eqeltri 2834 . . . . . . . . . . . . . . . . . . 19 (3 · 2) ∈ ℂ
295187, 249eqnetri 3014 . . . . . . . . . . . . . . . . . . 19 (3 · 2) ≠ 0
29687, 294, 287, 295divmuli 11909 . . . . . . . . . . . . . . . . . 18 ((2 / (3 · 2)) = (1 / 3) ↔ ((3 · 2) · (1 / 3)) = 2)
297293, 296mpbir 230 . . . . . . . . . . . . . . . . 17 (2 / (3 · 2)) = (1 / 3)
29887, 178, 249divreci 11900 . . . . . . . . . . . . . . . . 17 (2 / 6) = (2 · (1 / 6))
299286, 297, 2983eqtr3ri 2773 . . . . . . . . . . . . . . . 16 (2 · (1 / 6)) = (1 / 3)
300299a1i 11 . . . . . . . . . . . . . . 15 (𝑋 ∈ ℂ → (2 · (1 / 6)) = (1 / 3))
301285, 300oveq12d 7375 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → ((2 · ((𝑋↑2) − 𝑋)) + (2 · (1 / 6))) = (((2 · (𝑋↑2)) − (2 · 𝑋)) + (1 / 3)))
302284, 301eqtrd 2776 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (2 · (((𝑋↑2) − 𝑋) + (1 / 6))) = (((2 · (𝑋↑2)) − (2 · 𝑋)) + (1 / 3)))
303302oveq2d 7373 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → (𝑋 + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))) = (𝑋 + (((2 · (𝑋↑2)) − (2 · 𝑋)) + (1 / 3))))
304191, 224mulcld 11175 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → (2 · (𝑋↑2)) ∈ ℂ)
305191, 242mulcld 11175 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → (2 · 𝑋) ∈ ℂ)
306304, 305subcld 11512 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → ((2 · (𝑋↑2)) − (2 · 𝑋)) ∈ ℂ)
307287a1i 11 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (1 / 3) ∈ ℂ)
308242, 306, 307addassd 11177 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → ((𝑋 + ((2 · (𝑋↑2)) − (2 · 𝑋))) + (1 / 3)) = (𝑋 + (((2 · (𝑋↑2)) − (2 · 𝑋)) + (1 / 3))))
309242, 304, 305addsub12d 11535 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (𝑋 + ((2 · (𝑋↑2)) − (2 · 𝑋))) = ((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))))
310309oveq1d 7372 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → ((𝑋 + ((2 · (𝑋↑2)) − (2 · 𝑋))) + (1 / 3)) = (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3)))
311303, 308, 3103eqtr2d 2782 . . . . . . . . . . 11 (𝑋 ∈ ℂ → (𝑋 + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))) = (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3)))
312311oveq2d 7373 . . . . . . . . . 10 (𝑋 ∈ ℂ → (((1 / 5) + (𝑋 − (1 / 2))) + (𝑋 + (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))) = (((1 / 5) + (𝑋 − (1 / 2))) + (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3))))
313283, 312eqtrd 2776 . . . . . . . . 9 (𝑋 ∈ ℂ → (𝑋 + (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))) = (((1 / 5) + (𝑋 − (1 / 2))) + (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3))))
314313oveq2d 7373 . . . . . . . 8 (𝑋 ∈ ℂ → ((3 · (𝑋↑2)) − (𝑋 + (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))))) = ((3 · (𝑋↑2)) − (((1 / 5) + (𝑋 − (1 / 2))) + (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3)))))
315242, 305subcld 11512 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (𝑋 − (2 · 𝑋)) ∈ ℂ)
316304, 315addcld 11174 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → ((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) ∈ ℂ)
317241, 245, 316, 307add4d 11383 . . . . . . . . . . 11 (𝑋 ∈ ℂ → (((1 / 5) + (𝑋 − (1 / 2))) + (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3))) = (((1 / 5) + ((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋)))) + ((𝑋 − (1 / 2)) + (1 / 3))))
318241, 304, 315add12d 11381 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → ((1 / 5) + ((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋)))) = ((2 · (𝑋↑2)) + ((1 / 5) + (𝑋 − (2 · 𝑋)))))
319318oveq1d 7372 . . . . . . . . . . 11 (𝑋 ∈ ℂ → (((1 / 5) + ((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋)))) + ((𝑋 − (1 / 2)) + (1 / 3))) = (((2 · (𝑋↑2)) + ((1 / 5) + (𝑋 − (2 · 𝑋)))) + ((𝑋 − (1 / 2)) + (1 / 3))))
320241, 315addcld 11174 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → ((1 / 5) + (𝑋 − (2 · 𝑋))) ∈ ℂ)
321245, 307addcld 11174 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → ((𝑋 − (1 / 2)) + (1 / 3)) ∈ ℂ)
322304, 320, 321addassd 11177 . . . . . . . . . . 11 (𝑋 ∈ ℂ → (((2 · (𝑋↑2)) + ((1 / 5) + (𝑋 − (2 · 𝑋)))) + ((𝑋 − (1 / 2)) + (1 / 3))) = ((2 · (𝑋↑2)) + (((1 / 5) + (𝑋 − (2 · 𝑋))) + ((𝑋 − (1 / 2)) + (1 / 3)))))
323317, 319, 3223eqtrd 2780 . . . . . . . . . 10 (𝑋 ∈ ℂ → (((1 / 5) + (𝑋 − (1 / 2))) + (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3))) = ((2 · (𝑋↑2)) + (((1 / 5) + (𝑋 − (2 · 𝑋))) + ((𝑋 − (1 / 2)) + (1 / 3)))))
324323oveq2d 7373 . . . . . . . . 9 (𝑋 ∈ ℂ → ((3 · (𝑋↑2)) − (((1 / 5) + (𝑋 − (1 / 2))) + (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3)))) = ((3 · (𝑋↑2)) − ((2 · (𝑋↑2)) + (((1 / 5) + (𝑋 − (2 · 𝑋))) + ((𝑋 − (1 / 2)) + (1 / 3))))))
325183, 224mulcld 11175 . . . . . . . . . 10 (𝑋 ∈ ℂ → (3 · (𝑋↑2)) ∈ ℂ)
326320, 321addcld 11174 . . . . . . . . . 10 (𝑋 ∈ ℂ → (((1 / 5) + (𝑋 − (2 · 𝑋))) + ((𝑋 − (1 / 2)) + (1 / 3))) ∈ ℂ)
327325, 304, 326subsub4d 11543 . . . . . . . . 9 (𝑋 ∈ ℂ → (((3 · (𝑋↑2)) − (2 · (𝑋↑2))) − (((1 / 5) + (𝑋 − (2 · 𝑋))) + ((𝑋 − (1 / 2)) + (1 / 3)))) = ((3 · (𝑋↑2)) − ((2 · (𝑋↑2)) + (((1 / 5) + (𝑋 − (2 · 𝑋))) + ((𝑋 − (1 / 2)) + (1 / 3))))))
32858, 87, 59, 109subaddrii 11490 . . . . . . . . . . . 12 (3 − 2) = 1
329328oveq1i 7367 . . . . . . . . . . 11 ((3 − 2) · (𝑋↑2)) = (1 · (𝑋↑2))
330183, 191, 224subdird 11612 . . . . . . . . . . 11 (𝑋 ∈ ℂ → ((3 − 2) · (𝑋↑2)) = ((3 · (𝑋↑2)) − (2 · (𝑋↑2))))
331224mulid2d 11173 . . . . . . . . . . 11 (𝑋 ∈ ℂ → (1 · (𝑋↑2)) = (𝑋↑2))
332329, 330, 3313eqtr3a 2800 . . . . . . . . . 10 (𝑋 ∈ ℂ → ((3 · (𝑋↑2)) − (2 · (𝑋↑2))) = (𝑋↑2))
333241, 305, 242subsubd 11540 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → ((1 / 5) − ((2 · 𝑋) − 𝑋)) = (((1 / 5) − (2 · 𝑋)) + 𝑋))
334 2txmxeqx 12293 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → ((2 · 𝑋) − 𝑋) = 𝑋)
335334oveq2d 7373 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → ((1 / 5) − ((2 · 𝑋) − 𝑋)) = ((1 / 5) − 𝑋))
336241, 305, 242subadd23d 11534 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (((1 / 5) − (2 · 𝑋)) + 𝑋) = ((1 / 5) + (𝑋 − (2 · 𝑋))))
337333, 335, 3363eqtr3d 2784 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → ((1 / 5) − 𝑋) = ((1 / 5) + (𝑋 − (2 · 𝑋))))
338242, 244, 307subsubd 11540 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → (𝑋 − ((1 / 2) − (1 / 3))) = ((𝑋 − (1 / 2)) + (1 / 3)))
339337, 338oveq12d 7375 . . . . . . . . . . 11 (𝑋 ∈ ℂ → (((1 / 5) − 𝑋) + (𝑋 − ((1 / 2) − (1 / 3)))) = (((1 / 5) + (𝑋 − (2 · 𝑋))) + ((𝑋 − (1 / 2)) + (1 / 3))))
340243, 287subcli 11477 . . . . . . . . . . . . . 14 ((1 / 2) − (1 / 3)) ∈ ℂ
341340a1i 11 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → ((1 / 2) − (1 / 3)) ∈ ℂ)
342241, 242, 341npncand 11536 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → (((1 / 5) − 𝑋) + (𝑋 − ((1 / 2) − (1 / 3)))) = ((1 / 5) − ((1 / 2) − (1 / 3))))
343 halfthird 12761 . . . . . . . . . . . . . 14 ((1 / 2) − (1 / 3)) = (1 / 6)
344343oveq2i 7368 . . . . . . . . . . . . 13 ((1 / 5) − ((1 / 2) − (1 / 3))) = ((1 / 5) − (1 / 6))
345 5recm6rec 12762 . . . . . . . . . . . . 13 ((1 / 5) − (1 / 6)) = (1 / 30)
346344, 345eqtri 2764 . . . . . . . . . . . 12 ((1 / 5) − ((1 / 2) − (1 / 3))) = (1 / 30)
347342, 346eqtrdi 2792 . . . . . . . . . . 11 (𝑋 ∈ ℂ → (((1 / 5) − 𝑋) + (𝑋 − ((1 / 2) − (1 / 3)))) = (1 / 30))
348339, 347eqtr3d 2778 . . . . . . . . . 10 (𝑋 ∈ ℂ → (((1 / 5) + (𝑋 − (2 · 𝑋))) + ((𝑋 − (1 / 2)) + (1 / 3))) = (1 / 30))
349332, 348oveq12d 7375 . . . . . . . . 9 (𝑋 ∈ ℂ → (((3 · (𝑋↑2)) − (2 · (𝑋↑2))) − (((1 / 5) + (𝑋 − (2 · 𝑋))) + ((𝑋 − (1 / 2)) + (1 / 3)))) = ((𝑋↑2) − (1 / 30)))
350324, 327, 3493eqtr2d 2782 . . . . . . . 8 (𝑋 ∈ ℂ → ((3 · (𝑋↑2)) − (((1 / 5) + (𝑋 − (1 / 2))) + (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3)))) = ((𝑋↑2) − (1 / 30)))
351282, 314, 3503eqtrd 2780 . . . . . . 7 (𝑋 ∈ ℂ → ((2 · ((3 / 2) · (𝑋↑2))) − (𝑋 + (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))))) = ((𝑋↑2) − (1 / 30)))
352351oveq2d 7373 . . . . . 6 (𝑋 ∈ ℂ → ((2 · (𝑋↑3)) − ((2 · ((3 / 2) · (𝑋↑2))) − (𝑋 + (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))))) = ((2 · (𝑋↑3)) − ((𝑋↑2) − (1 / 30))))
353275, 277, 3523eqtr2d 2782 . . . . 5 (𝑋 ∈ ℂ → ((((2 · (𝑋↑3)) − (2 · ((3 / 2) · (𝑋↑2)))) + 𝑋) + (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))) = ((2 · (𝑋↑3)) − ((𝑋↑2) − (1 / 30))))
354262, 272, 3533eqtrd 2780 . . . 4 (𝑋 ∈ ℂ → ((((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))) + (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋)))) = ((2 · (𝑋↑3)) − ((𝑋↑2) − (1 / 30))))
355354oveq2d 7373 . . 3 (𝑋 ∈ ℂ → ((𝑋↑4) − ((((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))) + (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))))) = ((𝑋↑4) − ((2 · (𝑋↑3)) − ((𝑋↑2) − (1 / 30)))))
356220, 223subcld 11512 . . . 4 (𝑋 ∈ ℂ → ((𝑋↑4) − (2 · (𝑋↑3))) ∈ ℂ)
357356, 224, 238addsubassd 11532 . . 3 (𝑋 ∈ ℂ → ((((𝑋↑4) − (2 · (𝑋↑3))) + (𝑋↑2)) − (1 / 30)) = (((𝑋↑4) − (2 · (𝑋↑3))) + ((𝑋↑2) − (1 / 30))))
358240, 355, 3573eqtr4d 2786 . 2 (𝑋 ∈ ℂ → ((𝑋↑4) − ((((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))) + (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))))) = ((((𝑋↑4) − (2 · (𝑋↑3))) + (𝑋↑2)) − (1 / 30)))
3593, 218, 3583eqtrd 2780 1 (𝑋 ∈ ℂ → (4 BernPoly 𝑋) = ((((𝑋↑4) − (2 · (𝑋↑3))) + (𝑋↑2)) − (1 / 30)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  wcel 2106  wne 2943  wss 3910   class class class wbr 5105  cfv 6496  (class class class)co 7357  cc 11049  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056   < clt 11189  cmin 11385   / cdiv 11812  cn 12153  2c2 12208  3c3 12209  4c4 12210  5c5 12211  6c6 12212  0cn0 12413  cz 12499  cdc 12618  cuz 12763  ...cfz 13424  cexp 13967  Ccbc 14202  Σcsu 15570   BernPoly cbp 15929
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-sup 9378  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-rp 12916  df-fz 13425  df-fzo 13568  df-seq 13907  df-exp 13968  df-fac 14174  df-bc 14203  df-hash 14231  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-clim 15370  df-sum 15571  df-bpoly 15930
This theorem is referenced by:  fsumcube  15943
  Copyright terms: Public domain W3C validator