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

Theorem bpoly4 16095
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 12545 . . 3 4 ∈ ℕ0
2 bpolyval 16085 . . 3 ((4 ∈ ℕ0𝑋 ∈ ℂ) → (4 BernPoly 𝑋) = ((𝑋↑4) − Σ𝑘 ∈ (0...(4 − 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)))))
31, 2mpan 690 . 2 (𝑋 ∈ ℂ → (4 BernPoly 𝑋) = ((𝑋↑4) − Σ𝑘 ∈ (0...(4 − 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)))))
4 4m1e3 12395 . . . . . . 7 (4 − 1) = 3
5 df-3 12330 . . . . . . 7 3 = (2 + 1)
64, 5eqtri 2765 . . . . . 6 (4 − 1) = (2 + 1)
76oveq2i 7442 . . . . 5 (0...(4 − 1)) = (0...(2 + 1))
87sumeq1i 15733 . . . 4 Σ𝑘 ∈ (0...(4 − 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = Σ𝑘 ∈ (0...(2 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)))
9 2eluzge0 12935 . . . . . . 7 2 ∈ (ℤ‘0)
109a1i 11 . . . . . 6 (𝑋 ∈ ℂ → 2 ∈ (ℤ‘0))
11 elfzelz 13564 . . . . . . . . . 10 (𝑘 ∈ (0...(2 + 1)) → 𝑘 ∈ ℤ)
12 bccl 14361 . . . . . . . . . 10 ((4 ∈ ℕ0𝑘 ∈ ℤ) → (4C𝑘) ∈ ℕ0)
131, 11, 12sylancr 587 . . . . . . . . 9 (𝑘 ∈ (0...(2 + 1)) → (4C𝑘) ∈ ℕ0)
1413nn0cnd 12589 . . . . . . . 8 (𝑘 ∈ (0...(2 + 1)) → (4C𝑘) ∈ ℂ)
1514adantl 481 . . . . . . 7 ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(2 + 1))) → (4C𝑘) ∈ ℂ)
16 elfznn0 13660 . . . . . . . . . 10 (𝑘 ∈ (0...(2 + 1)) → 𝑘 ∈ ℕ0)
17 bpolycl 16088 . . . . . . . . . 10 ((𝑘 ∈ ℕ0𝑋 ∈ ℂ) → (𝑘 BernPoly 𝑋) ∈ ℂ)
1816, 17sylan 580 . . . . . . . . 9 ((𝑘 ∈ (0...(2 + 1)) ∧ 𝑋 ∈ ℂ) → (𝑘 BernPoly 𝑋) ∈ ℂ)
1918ancoms 458 . . . . . . . 8 ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(2 + 1))) → (𝑘 BernPoly 𝑋) ∈ ℂ)
20 4re 12350 . . . . . . . . . . . . 13 4 ∈ ℝ
2120a1i 11 . . . . . . . . . . . 12 (𝑘 ∈ (0...(2 + 1)) → 4 ∈ ℝ)
2211zred 12722 . . . . . . . . . . . 12 (𝑘 ∈ (0...(2 + 1)) → 𝑘 ∈ ℝ)
2321, 22resubcld 11691 . . . . . . . . . . 11 (𝑘 ∈ (0...(2 + 1)) → (4 − 𝑘) ∈ ℝ)
24 peano2re 11434 . . . . . . . . . . 11 ((4 − 𝑘) ∈ ℝ → ((4 − 𝑘) + 1) ∈ ℝ)
2523, 24syl 17 . . . . . . . . . 10 (𝑘 ∈ (0...(2 + 1)) → ((4 − 𝑘) + 1) ∈ ℝ)
2625recnd 11289 . . . . . . . . 9 (𝑘 ∈ (0...(2 + 1)) → ((4 − 𝑘) + 1) ∈ ℂ)
2726adantl 481 . . . . . . . 8 ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(2 + 1))) → ((4 − 𝑘) + 1) ∈ ℂ)
28 1red 11262 . . . . . . . . . . 11 (𝑘 ∈ (0...(2 + 1)) → 1 ∈ ℝ)
295oveq2i 7442 . . . . . . . . . . . . . 14 (0...3) = (0...(2 + 1))
3029eleq2i 2833 . . . . . . . . . . . . 13 (𝑘 ∈ (0...3) ↔ 𝑘 ∈ (0...(2 + 1)))
31 elfzelz 13564 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...3) → 𝑘 ∈ ℤ)
3231zred 12722 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...3) → 𝑘 ∈ ℝ)
33 3re 12346 . . . . . . . . . . . . . . 15 3 ∈ ℝ
3433a1i 11 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...3) → 3 ∈ ℝ)
3520a1i 11 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...3) → 4 ∈ ℝ)
36 elfzle2 13568 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...3) → 𝑘 ≤ 3)
37 3lt4 12440 . . . . . . . . . . . . . . 15 3 < 4
3837a1i 11 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...3) → 3 < 4)
3932, 34, 35, 36, 38lelttrd 11419 . . . . . . . . . . . . 13 (𝑘 ∈ (0...3) → 𝑘 < 4)
4030, 39sylbir 235 . . . . . . . . . . . 12 (𝑘 ∈ (0...(2 + 1)) → 𝑘 < 4)
4122, 21posdifd 11850 . . . . . . . . . . . 12 (𝑘 ∈ (0...(2 + 1)) → (𝑘 < 4 ↔ 0 < (4 − 𝑘)))
4240, 41mpbid 232 . . . . . . . . . . 11 (𝑘 ∈ (0...(2 + 1)) → 0 < (4 − 𝑘))
43 0lt1 11785 . . . . . . . . . . . 12 0 < 1
4443a1i 11 . . . . . . . . . . 11 (𝑘 ∈ (0...(2 + 1)) → 0 < 1)
4523, 28, 42, 44addgt0d 11838 . . . . . . . . . 10 (𝑘 ∈ (0...(2 + 1)) → 0 < ((4 − 𝑘) + 1))
4645gt0ne0d 11827 . . . . . . . . 9 (𝑘 ∈ (0...(2 + 1)) → ((4 − 𝑘) + 1) ≠ 0)
4746adantl 481 . . . . . . . 8 ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(2 + 1))) → ((4 − 𝑘) + 1) ≠ 0)
4819, 27, 47divcld 12043 . . . . . . 7 ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(2 + 1))) → ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)) ∈ ℂ)
4915, 48mulcld 11281 . . . . . 6 ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(2 + 1))) → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) ∈ ℂ)
505eqeq2i 2750 . . . . . . 7 (𝑘 = 3 ↔ 𝑘 = (2 + 1))
51 oveq2 7439 . . . . . . . . 9 (𝑘 = 3 → (4C𝑘) = (4C3))
52 4bc3eq4 14367 . . . . . . . . 9 (4C3) = 4
5351, 52eqtrdi 2793 . . . . . . . 8 (𝑘 = 3 → (4C𝑘) = 4)
54 oveq1 7438 . . . . . . . . 9 (𝑘 = 3 → (𝑘 BernPoly 𝑋) = (3 BernPoly 𝑋))
55 oveq2 7439 . . . . . . . . . . 11 (𝑘 = 3 → (4 − 𝑘) = (4 − 3))
5655oveq1d 7446 . . . . . . . . . 10 (𝑘 = 3 → ((4 − 𝑘) + 1) = ((4 − 3) + 1))
57 4cn 12351 . . . . . . . . . . . . 13 4 ∈ ℂ
58 3cn 12347 . . . . . . . . . . . . 13 3 ∈ ℂ
59 ax-1cn 11213 . . . . . . . . . . . . 13 1 ∈ ℂ
60 3p1e4 12411 . . . . . . . . . . . . 13 (3 + 1) = 4
6157, 58, 59, 60subaddrii 11598 . . . . . . . . . . . 12 (4 − 3) = 1
6261oveq1i 7441 . . . . . . . . . . 11 ((4 − 3) + 1) = (1 + 1)
63 df-2 12329 . . . . . . . . . . 11 2 = (1 + 1)
6462, 63eqtr4i 2768 . . . . . . . . . 10 ((4 − 3) + 1) = 2
6556, 64eqtrdi 2793 . . . . . . . . 9 (𝑘 = 3 → ((4 − 𝑘) + 1) = 2)
6654, 65oveq12d 7449 . . . . . . . 8 (𝑘 = 3 → ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)) = ((3 BernPoly 𝑋) / 2))
6753, 66oveq12d 7449 . . . . . . 7 (𝑘 = 3 → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (4 · ((3 BernPoly 𝑋) / 2)))
6850, 67sylbir 235 . . . . . 6 (𝑘 = (2 + 1) → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (4 · ((3 BernPoly 𝑋) / 2)))
6910, 49, 68fsump1 15792 . . . . 5 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...(2 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (Σ𝑘 ∈ (0...2)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) + (4 · ((3 BernPoly 𝑋) / 2))))
7063oveq2i 7442 . . . . . . . 8 (0...2) = (0...(1 + 1))
7170sumeq1i 15733 . . . . . . 7 Σ𝑘 ∈ (0...2)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = Σ𝑘 ∈ (0...(1 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)))
72 1eluzge0 12934 . . . . . . . . . 10 1 ∈ (ℤ‘0)
7372a1i 11 . . . . . . . . 9 (𝑋 ∈ ℂ → 1 ∈ (ℤ‘0))
74 fzssp1 13607 . . . . . . . . . . . 12 (0...(1 + 1)) ⊆ (0...((1 + 1) + 1))
7563oveq1i 7441 . . . . . . . . . . . . 13 (2 + 1) = ((1 + 1) + 1)
7675oveq2i 7442 . . . . . . . . . . . 12 (0...(2 + 1)) = (0...((1 + 1) + 1))
7774, 76sseqtrri 4033 . . . . . . . . . . 11 (0...(1 + 1)) ⊆ (0...(2 + 1))
7877sseli 3979 . . . . . . . . . 10 (𝑘 ∈ (0...(1 + 1)) → 𝑘 ∈ (0...(2 + 1)))
7978, 49sylan2 593 . . . . . . . . 9 ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(1 + 1))) → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) ∈ ℂ)
8063eqeq2i 2750 . . . . . . . . . 10 (𝑘 = 2 ↔ 𝑘 = (1 + 1))
81 oveq2 7439 . . . . . . . . . . . 12 (𝑘 = 2 → (4C𝑘) = (4C2))
82 4bc2eq6 14368 . . . . . . . . . . . 12 (4C2) = 6
8381, 82eqtrdi 2793 . . . . . . . . . . 11 (𝑘 = 2 → (4C𝑘) = 6)
84 oveq1 7438 . . . . . . . . . . . 12 (𝑘 = 2 → (𝑘 BernPoly 𝑋) = (2 BernPoly 𝑋))
85 oveq2 7439 . . . . . . . . . . . . . 14 (𝑘 = 2 → (4 − 𝑘) = (4 − 2))
8685oveq1d 7446 . . . . . . . . . . . . 13 (𝑘 = 2 → ((4 − 𝑘) + 1) = ((4 − 2) + 1))
87 2cn 12341 . . . . . . . . . . . . . . . 16 2 ∈ ℂ
88 2p2e4 12401 . . . . . . . . . . . . . . . 16 (2 + 2) = 4
8957, 87, 87, 88subaddrii 11598 . . . . . . . . . . . . . . 15 (4 − 2) = 2
9089oveq1i 7441 . . . . . . . . . . . . . 14 ((4 − 2) + 1) = (2 + 1)
9190, 5eqtr4i 2768 . . . . . . . . . . . . 13 ((4 − 2) + 1) = 3
9286, 91eqtrdi 2793 . . . . . . . . . . . 12 (𝑘 = 2 → ((4 − 𝑘) + 1) = 3)
9384, 92oveq12d 7449 . . . . . . . . . . 11 (𝑘 = 2 → ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)) = ((2 BernPoly 𝑋) / 3))
9483, 93oveq12d 7449 . . . . . . . . . 10 (𝑘 = 2 → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (6 · ((2 BernPoly 𝑋) / 3)))
9580, 94sylbir 235 . . . . . . . . 9 (𝑘 = (1 + 1) → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (6 · ((2 BernPoly 𝑋) / 3)))
9673, 79, 95fsump1 15792 . . . . . . . 8 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...(1 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (Σ𝑘 ∈ (0...1)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) + (6 · ((2 BernPoly 𝑋) / 3))))
97 0p1e1 12388 . . . . . . . . . . . 12 (0 + 1) = 1
9897oveq2i 7442 . . . . . . . . . . 11 (0...(0 + 1)) = (0...1)
9998sumeq1i 15733 . . . . . . . . . 10 Σ𝑘 ∈ (0...(0 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = Σ𝑘 ∈ (0...1)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)))
100 0nn0 12541 . . . . . . . . . . . . . 14 0 ∈ ℕ0
101 nn0uz 12920 . . . . . . . . . . . . . 14 0 = (ℤ‘0)
102100, 101eleqtri 2839 . . . . . . . . . . . . 13 0 ∈ (ℤ‘0)
103102a1i 11 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → 0 ∈ (ℤ‘0))
104 3nn 12345 . . . . . . . . . . . . . . . . 17 3 ∈ ℕ
105 nnuz 12921 . . . . . . . . . . . . . . . . 17 ℕ = (ℤ‘1)
106104, 105eleqtri 2839 . . . . . . . . . . . . . . . 16 3 ∈ (ℤ‘1)
107 fzss2 13604 . . . . . . . . . . . . . . . 16 (3 ∈ (ℤ‘1) → (0...1) ⊆ (0...3))
108106, 107ax-mp 5 . . . . . . . . . . . . . . 15 (0...1) ⊆ (0...3)
109 2p1e3 12408 . . . . . . . . . . . . . . . 16 (2 + 1) = 3
110109oveq2i 7442 . . . . . . . . . . . . . . 15 (0...(2 + 1)) = (0...3)
111108, 98, 1103sstr4i 4035 . . . . . . . . . . . . . 14 (0...(0 + 1)) ⊆ (0...(2 + 1))
112111sseli 3979 . . . . . . . . . . . . 13 (𝑘 ∈ (0...(0 + 1)) → 𝑘 ∈ (0...(2 + 1)))
113112, 49sylan2 593 . . . . . . . . . . . 12 ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(0 + 1))) → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) ∈ ℂ)
11497eqeq2i 2750 . . . . . . . . . . . . 13 (𝑘 = (0 + 1) ↔ 𝑘 = 1)
115 oveq2 7439 . . . . . . . . . . . . . . 15 (𝑘 = 1 → (4C𝑘) = (4C1))
116 bcn1 14352 . . . . . . . . . . . . . . . 16 (4 ∈ ℕ0 → (4C1) = 4)
1171, 116ax-mp 5 . . . . . . . . . . . . . . 15 (4C1) = 4
118115, 117eqtrdi 2793 . . . . . . . . . . . . . 14 (𝑘 = 1 → (4C𝑘) = 4)
119 oveq1 7438 . . . . . . . . . . . . . . 15 (𝑘 = 1 → (𝑘 BernPoly 𝑋) = (1 BernPoly 𝑋))
120 oveq2 7439 . . . . . . . . . . . . . . . . 17 (𝑘 = 1 → (4 − 𝑘) = (4 − 1))
121120oveq1d 7446 . . . . . . . . . . . . . . . 16 (𝑘 = 1 → ((4 − 𝑘) + 1) = ((4 − 1) + 1))
1224oveq1i 7441 . . . . . . . . . . . . . . . . 17 ((4 − 1) + 1) = (3 + 1)
123 df-4 12331 . . . . . . . . . . . . . . . . 17 4 = (3 + 1)
124122, 123eqtr4i 2768 . . . . . . . . . . . . . . . 16 ((4 − 1) + 1) = 4
125121, 124eqtrdi 2793 . . . . . . . . . . . . . . 15 (𝑘 = 1 → ((4 − 𝑘) + 1) = 4)
126119, 125oveq12d 7449 . . . . . . . . . . . . . 14 (𝑘 = 1 → ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)) = ((1 BernPoly 𝑋) / 4))
127118, 126oveq12d 7449 . . . . . . . . . . . . 13 (𝑘 = 1 → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (4 · ((1 BernPoly 𝑋) / 4)))
128114, 127sylbi 217 . . . . . . . . . . . 12 (𝑘 = (0 + 1) → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (4 · ((1 BernPoly 𝑋) / 4)))
129103, 113, 128fsump1 15792 . . . . . . . . . . 11 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...(0 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (Σ𝑘 ∈ (0...0)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) + (4 · ((1 BernPoly 𝑋) / 4))))
130 0z 12624 . . . . . . . . . . . . . 14 0 ∈ ℤ
13159a1i 11 . . . . . . . . . . . . . . 15 (𝑋 ∈ ℂ → 1 ∈ ℂ)
132 bpolycl 16088 . . . . . . . . . . . . . . . . 17 ((0 ∈ ℕ0𝑋 ∈ ℂ) → (0 BernPoly 𝑋) ∈ ℂ)
133100, 132mpan 690 . . . . . . . . . . . . . . . 16 (𝑋 ∈ ℂ → (0 BernPoly 𝑋) ∈ ℂ)
134 5cn 12354 . . . . . . . . . . . . . . . . 17 5 ∈ ℂ
135134a1i 11 . . . . . . . . . . . . . . . 16 (𝑋 ∈ ℂ → 5 ∈ ℂ)
136 0re 11263 . . . . . . . . . . . . . . . . . 18 0 ∈ ℝ
137 5pos 12375 . . . . . . . . . . . . . . . . . 18 0 < 5
138136, 137gtneii 11373 . . . . . . . . . . . . . . . . 17 5 ≠ 0
139138a1i 11 . . . . . . . . . . . . . . . 16 (𝑋 ∈ ℂ → 5 ≠ 0)
140133, 135, 139divcld 12043 . . . . . . . . . . . . . . 15 (𝑋 ∈ ℂ → ((0 BernPoly 𝑋) / 5) ∈ ℂ)
141131, 140mulcld 11281 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → (1 · ((0 BernPoly 𝑋) / 5)) ∈ ℂ)
142 oveq2 7439 . . . . . . . . . . . . . . . . 17 (𝑘 = 0 → (4C𝑘) = (4C0))
143 bcn0 14349 . . . . . . . . . . . . . . . . . 18 (4 ∈ ℕ0 → (4C0) = 1)
1441, 143ax-mp 5 . . . . . . . . . . . . . . . . 17 (4C0) = 1
145142, 144eqtrdi 2793 . . . . . . . . . . . . . . . 16 (𝑘 = 0 → (4C𝑘) = 1)
146 oveq1 7438 . . . . . . . . . . . . . . . . 17 (𝑘 = 0 → (𝑘 BernPoly 𝑋) = (0 BernPoly 𝑋))
147 oveq2 7439 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 0 → (4 − 𝑘) = (4 − 0))
148147oveq1d 7446 . . . . . . . . . . . . . . . . . 18 (𝑘 = 0 → ((4 − 𝑘) + 1) = ((4 − 0) + 1))
14957subid1i 11581 . . . . . . . . . . . . . . . . . . . 20 (4 − 0) = 4
150149oveq1i 7441 . . . . . . . . . . . . . . . . . . 19 ((4 − 0) + 1) = (4 + 1)
151 4p1e5 12412 . . . . . . . . . . . . . . . . . . 19 (4 + 1) = 5
152150, 151eqtri 2765 . . . . . . . . . . . . . . . . . 18 ((4 − 0) + 1) = 5
153148, 152eqtrdi 2793 . . . . . . . . . . . . . . . . 17 (𝑘 = 0 → ((4 − 𝑘) + 1) = 5)
154146, 153oveq12d 7449 . . . . . . . . . . . . . . . 16 (𝑘 = 0 → ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)) = ((0 BernPoly 𝑋) / 5))
155145, 154oveq12d 7449 . . . . . . . . . . . . . . 15 (𝑘 = 0 → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (1 · ((0 BernPoly 𝑋) / 5)))
156155fsum1 15783 . . . . . . . . . . . . . 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 16086 . . . . . . . . . . . . . . . 16 (𝑋 ∈ ℂ → (0 BernPoly 𝑋) = 1)
159158oveq1d 7446 . . . . . . . . . . . . . . 15 (𝑋 ∈ ℂ → ((0 BernPoly 𝑋) / 5) = (1 / 5))
160159oveq2d 7447 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → (1 · ((0 BernPoly 𝑋) / 5)) = (1 · (1 / 5)))
161134, 138reccli 11997 . . . . . . . . . . . . . . 15 (1 / 5) ∈ ℂ
162161mullidi 11266 . . . . . . . . . . . . . 14 (1 · (1 / 5)) = (1 / 5)
163160, 162eqtrdi 2793 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (1 · ((0 BernPoly 𝑋) / 5)) = (1 / 5))
164157, 163eqtrd 2777 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...0)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (1 / 5))
165 1nn0 12542 . . . . . . . . . . . . . . 15 1 ∈ ℕ0
166 bpolycl 16088 . . . . . . . . . . . . . . 15 ((1 ∈ ℕ0𝑋 ∈ ℂ) → (1 BernPoly 𝑋) ∈ ℂ)
167165, 166mpan 690 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → (1 BernPoly 𝑋) ∈ ℂ)
168 nn0cn 12536 . . . . . . . . . . . . . . 15 (4 ∈ ℕ0 → 4 ∈ ℂ)
1691, 168mp1i 13 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → 4 ∈ ℂ)
170 4ne0 12374 . . . . . . . . . . . . . . 15 4 ≠ 0
171170a1i 11 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → 4 ≠ 0)
172167, 169, 171divcan2d 12045 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (4 · ((1 BernPoly 𝑋) / 4)) = (1 BernPoly 𝑋))
173 bpoly1 16087 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (1 BernPoly 𝑋) = (𝑋 − (1 / 2)))
174172, 173eqtrd 2777 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → (4 · ((1 BernPoly 𝑋) / 4)) = (𝑋 − (1 / 2)))
175164, 174oveq12d 7449 . . . . . . . . . . 11 (𝑋 ∈ ℂ → (Σ𝑘 ∈ (0...0)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) + (4 · ((1 BernPoly 𝑋) / 4))) = ((1 / 5) + (𝑋 − (1 / 2))))
176129, 175eqtrd 2777 . . . . . . . . . 10 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...(0 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = ((1 / 5) + (𝑋 − (1 / 2))))
17799, 176eqtr3id 2791 . . . . . . . . 9 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...1)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = ((1 / 5) + (𝑋 − (1 / 2))))
178 6cn 12357 . . . . . . . . . . . 12 6 ∈ ℂ
179178a1i 11 . . . . . . . . . . 11 (𝑋 ∈ ℂ → 6 ∈ ℂ)
180 2nn0 12543 . . . . . . . . . . . 12 2 ∈ ℕ0
181 bpolycl 16088 . . . . . . . . . . . 12 ((2 ∈ ℕ0𝑋 ∈ ℂ) → (2 BernPoly 𝑋) ∈ ℂ)
182180, 181mpan 690 . . . . . . . . . . 11 (𝑋 ∈ ℂ → (2 BernPoly 𝑋) ∈ ℂ)
18358a1i 11 . . . . . . . . . . 11 (𝑋 ∈ ℂ → 3 ∈ ℂ)
184 3ne0 12372 . . . . . . . . . . . 12 3 ≠ 0
185184a1i 11 . . . . . . . . . . 11 (𝑋 ∈ ℂ → 3 ≠ 0)
186179, 182, 183, 185div12d 12079 . . . . . . . . . 10 (𝑋 ∈ ℂ → (6 · ((2 BernPoly 𝑋) / 3)) = ((2 BernPoly 𝑋) · (6 / 3)))
187 3t2e6 12432 . . . . . . . . . . . . 13 (3 · 2) = 6
188178, 58, 87, 184divmuli 12021 . . . . . . . . . . . . 13 ((6 / 3) = 2 ↔ (3 · 2) = 6)
189187, 188mpbir 231 . . . . . . . . . . . 12 (6 / 3) = 2
190189oveq2i 7442 . . . . . . . . . . 11 ((2 BernPoly 𝑋) · (6 / 3)) = ((2 BernPoly 𝑋) · 2)
19187a1i 11 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → 2 ∈ ℂ)
192182, 191mulcomd 11282 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → ((2 BernPoly 𝑋) · 2) = (2 · (2 BernPoly 𝑋)))
193 bpoly2 16093 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (2 BernPoly 𝑋) = (((𝑋↑2) − 𝑋) + (1 / 6)))
194193oveq2d 7447 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → (2 · (2 BernPoly 𝑋)) = (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))
195192, 194eqtrd 2777 . . . . . . . . . . 11 (𝑋 ∈ ℂ → ((2 BernPoly 𝑋) · 2) = (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))
196190, 195eqtrid 2789 . . . . . . . . . 10 (𝑋 ∈ ℂ → ((2 BernPoly 𝑋) · (6 / 3)) = (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))
197186, 196eqtrd 2777 . . . . . . . . 9 (𝑋 ∈ ℂ → (6 · ((2 BernPoly 𝑋) / 3)) = (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))
198177, 197oveq12d 7449 . . . . . . . 8 (𝑋 ∈ ℂ → (Σ𝑘 ∈ (0...1)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) + (6 · ((2 BernPoly 𝑋) / 3))) = (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))))
19996, 198eqtrd 2777 . . . . . . 7 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...(1 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))))
20071, 199eqtrid 2789 . . . . . 6 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...2)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))))
201 3nn0 12544 . . . . . . . . 9 3 ∈ ℕ0
202 bpolycl 16088 . . . . . . . . 9 ((3 ∈ ℕ0𝑋 ∈ ℂ) → (3 BernPoly 𝑋) ∈ ℂ)
203201, 202mpan 690 . . . . . . . 8 (𝑋 ∈ ℂ → (3 BernPoly 𝑋) ∈ ℂ)
204 2ne0 12370 . . . . . . . . 9 2 ≠ 0
205204a1i 11 . . . . . . . 8 (𝑋 ∈ ℂ → 2 ≠ 0)
206169, 203, 191, 205div12d 12079 . . . . . . 7 (𝑋 ∈ ℂ → (4 · ((3 BernPoly 𝑋) / 2)) = ((3 BernPoly 𝑋) · (4 / 2)))
207 4d2e2 12436 . . . . . . . . 9 (4 / 2) = 2
208207oveq2i 7442 . . . . . . . 8 ((3 BernPoly 𝑋) · (4 / 2)) = ((3 BernPoly 𝑋) · 2)
209203, 191mulcomd 11282 . . . . . . . . 9 (𝑋 ∈ ℂ → ((3 BernPoly 𝑋) · 2) = (2 · (3 BernPoly 𝑋)))
210 bpoly3 16094 . . . . . . . . . 10 (𝑋 ∈ ℂ → (3 BernPoly 𝑋) = (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋)))
211210oveq2d 7447 . . . . . . . . 9 (𝑋 ∈ ℂ → (2 · (3 BernPoly 𝑋)) = (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))))
212209, 211eqtrd 2777 . . . . . . . 8 (𝑋 ∈ ℂ → ((3 BernPoly 𝑋) · 2) = (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))))
213208, 212eqtrid 2789 . . . . . . 7 (𝑋 ∈ ℂ → ((3 BernPoly 𝑋) · (4 / 2)) = (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))))
214206, 213eqtrd 2777 . . . . . 6 (𝑋 ∈ ℂ → (4 · ((3 BernPoly 𝑋) / 2)) = (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))))
215200, 214oveq12d 7449 . . . . 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 2777 . . . 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 2789 . . 3 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...(4 − 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = ((((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))) + (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋)))))
218217oveq2d 7447 . 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 14120 . . . . 5 ((𝑋 ∈ ℂ ∧ 4 ∈ ℕ0) → (𝑋↑4) ∈ ℂ)
2201, 219mpan2 691 . . . 4 (𝑋 ∈ ℂ → (𝑋↑4) ∈ ℂ)
221 expcl 14120 . . . . . 6 ((𝑋 ∈ ℂ ∧ 3 ∈ ℕ0) → (𝑋↑3) ∈ ℂ)
222201, 221mpan2 691 . . . . 5 (𝑋 ∈ ℂ → (𝑋↑3) ∈ ℂ)
223191, 222mulcld 11281 . . . 4 (𝑋 ∈ ℂ → (2 · (𝑋↑3)) ∈ ℂ)
224 sqcl 14158 . . . . 5 (𝑋 ∈ ℂ → (𝑋↑2) ∈ ℂ)
225201, 100deccl 12748 . . . . . . . 8 30 ∈ ℕ0
226225nn0cni 12538 . . . . . . 7 30 ∈ ℂ
227 dfdec10 12736 . . . . . . . . 9 30 = ((10 · 3) + 0)
228 10re 12752 . . . . . . . . . . . 12 10 ∈ ℝ
229228recni 11275 . . . . . . . . . . 11 10 ∈ ℂ
230229, 58mulcli 11268 . . . . . . . . . 10 (10 · 3) ∈ ℂ
231230addridi 11448 . . . . . . . . 9 ((10 · 3) + 0) = (10 · 3)
232227, 231eqtri 2765 . . . . . . . 8 30 = (10 · 3)
233 10pos 12750 . . . . . . . . . 10 0 < 10
234136, 233gtneii 11373 . . . . . . . . 9 10 ≠ 0
235229, 58, 234, 184mulne0i 11906 . . . . . . . 8 (10 · 3) ≠ 0
236232, 235eqnetri 3011 . . . . . . 7 30 ≠ 0
237226, 236reccli 11997 . . . . . 6 (1 / 30) ∈ ℂ
238237a1i 11 . . . . 5 (𝑋 ∈ ℂ → (1 / 30) ∈ ℂ)
239224, 238subcld 11620 . . . 4 (𝑋 ∈ ℂ → ((𝑋↑2) − (1 / 30)) ∈ ℂ)
240220, 223, 239subsubd 11648 . . 3 (𝑋 ∈ ℂ → ((𝑋↑4) − ((2 · (𝑋↑3)) − ((𝑋↑2) − (1 / 30)))) = (((𝑋↑4) − (2 · (𝑋↑3))) + ((𝑋↑2) − (1 / 30))))
241161a1i 11 . . . . . . . 8 (𝑋 ∈ ℂ → (1 / 5) ∈ ℂ)
242 id 22 . . . . . . . . 9 (𝑋 ∈ ℂ → 𝑋 ∈ ℂ)
24387, 204reccli 11997 . . . . . . . . . 10 (1 / 2) ∈ ℂ
244243a1i 11 . . . . . . . . 9 (𝑋 ∈ ℂ → (1 / 2) ∈ ℂ)
245242, 244subcld 11620 . . . . . . . 8 (𝑋 ∈ ℂ → (𝑋 − (1 / 2)) ∈ ℂ)
246241, 245addcld 11280 . . . . . . 7 (𝑋 ∈ ℂ → ((1 / 5) + (𝑋 − (1 / 2))) ∈ ℂ)
247224, 242subcld 11620 . . . . . . . . 9 (𝑋 ∈ ℂ → ((𝑋↑2) − 𝑋) ∈ ℂ)
248 6pos 12376 . . . . . . . . . . . 12 0 < 6
249136, 248gtneii 11373 . . . . . . . . . . 11 6 ≠ 0
250178, 249reccli 11997 . . . . . . . . . 10 (1 / 6) ∈ ℂ
251250a1i 11 . . . . . . . . 9 (𝑋 ∈ ℂ → (1 / 6) ∈ ℂ)
252247, 251addcld 11280 . . . . . . . 8 (𝑋 ∈ ℂ → (((𝑋↑2) − 𝑋) + (1 / 6)) ∈ ℂ)
253191, 252mulcld 11281 . . . . . . 7 (𝑋 ∈ ℂ → (2 · (((𝑋↑2) − 𝑋) + (1 / 6))) ∈ ℂ)
254246, 253addcld 11280 . . . . . 6 (𝑋 ∈ ℂ → (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))) ∈ ℂ)
25558, 87, 204divcli 12009 . . . . . . . . . . 11 (3 / 2) ∈ ℂ
256255a1i 11 . . . . . . . . . 10 (𝑋 ∈ ℂ → (3 / 2) ∈ ℂ)
257256, 224mulcld 11281 . . . . . . . . 9 (𝑋 ∈ ℂ → ((3 / 2) · (𝑋↑2)) ∈ ℂ)
258222, 257subcld 11620 . . . . . . . 8 (𝑋 ∈ ℂ → ((𝑋↑3) − ((3 / 2) · (𝑋↑2))) ∈ ℂ)
259244, 242mulcld 11281 . . . . . . . 8 (𝑋 ∈ ℂ → ((1 / 2) · 𝑋) ∈ ℂ)
260258, 259addcld 11280 . . . . . . 7 (𝑋 ∈ ℂ → (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋)) ∈ ℂ)
261191, 260mulcld 11281 . . . . . 6 (𝑋 ∈ ℂ → (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))) ∈ ℂ)
262254, 261addcomd 11463 . . . . 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 11285 . . . . . . 7 (𝑋 ∈ ℂ → (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))) = ((2 · ((𝑋↑3) − ((3 / 2) · (𝑋↑2)))) + (2 · ((1 / 2) · 𝑋))))
264191, 222, 257subdid 11719 . . . . . . . 8 (𝑋 ∈ ℂ → (2 · ((𝑋↑3) − ((3 / 2) · (𝑋↑2)))) = ((2 · (𝑋↑3)) − (2 · ((3 / 2) · (𝑋↑2)))))
26587, 204recidi 11998 . . . . . . . . . 10 (2 · (1 / 2)) = 1
266265oveq1i 7441 . . . . . . . . 9 ((2 · (1 / 2)) · 𝑋) = (1 · 𝑋)
267191, 244, 242mulassd 11284 . . . . . . . . 9 (𝑋 ∈ ℂ → ((2 · (1 / 2)) · 𝑋) = (2 · ((1 / 2) · 𝑋)))
268 mullid 11260 . . . . . . . . 9 (𝑋 ∈ ℂ → (1 · 𝑋) = 𝑋)
269266, 267, 2683eqtr3a 2801 . . . . . . . 8 (𝑋 ∈ ℂ → (2 · ((1 / 2) · 𝑋)) = 𝑋)
270264, 269oveq12d 7449 . . . . . . 7 (𝑋 ∈ ℂ → ((2 · ((𝑋↑3) − ((3 / 2) · (𝑋↑2)))) + (2 · ((1 / 2) · 𝑋))) = (((2 · (𝑋↑3)) − (2 · ((3 / 2) · (𝑋↑2)))) + 𝑋))
271263, 270eqtrd 2777 . . . . . 6 (𝑋 ∈ ℂ → (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))) = (((2 · (𝑋↑3)) − (2 · ((3 / 2) · (𝑋↑2)))) + 𝑋))
272271oveq1d 7446 . . . . 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 11281 . . . . . . . 8 (𝑋 ∈ ℂ → (2 · ((3 / 2) · (𝑋↑2))) ∈ ℂ)
274223, 273subcld 11620 . . . . . . 7 (𝑋 ∈ ℂ → ((2 · (𝑋↑3)) − (2 · ((3 / 2) · (𝑋↑2)))) ∈ ℂ)
275274, 242, 254addassd 11283 . . . . . 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 11280 . . . . . . 7 (𝑋 ∈ ℂ → (𝑋 + (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))) ∈ ℂ)
277223, 273, 276subsubd 11648 . . . . . 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 11284 . . . . . . . . . 10 (𝑋 ∈ ℂ → ((2 · (3 / 2)) · (𝑋↑2)) = (2 · ((3 / 2) · (𝑋↑2))))
27958, 87, 204divcan2i 12010 . . . . . . . . . . 11 (2 · (3 / 2)) = 3
280279oveq1i 7441 . . . . . . . . . 10 ((2 · (3 / 2)) · (𝑋↑2)) = (3 · (𝑋↑2))
281278, 280eqtr3di 2792 . . . . . . . . 9 (𝑋 ∈ ℂ → (2 · ((3 / 2) · (𝑋↑2))) = (3 · (𝑋↑2)))
282281oveq1d 7446 . . . . . . . 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 11488 . . . . . . . . . 10 (𝑋 ∈ ℂ → (𝑋 + (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))) = (((1 / 5) + (𝑋 − (1 / 2))) + (𝑋 + (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))))
284191, 247, 251adddid 11285 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → (2 · (((𝑋↑2) − 𝑋) + (1 / 6))) = ((2 · ((𝑋↑2) − 𝑋)) + (2 · (1 / 6))))
285191, 224, 242subdid 11719 . . . . . . . . . . . . . . 15 (𝑋 ∈ ℂ → (2 · ((𝑋↑2) − 𝑋)) = ((2 · (𝑋↑2)) − (2 · 𝑋)))
286187oveq2i 7442 . . . . . . . . . . . . . . . . 17 (2 / (3 · 2)) = (2 / 6)
28758, 184reccli 11997 . . . . . . . . . . . . . . . . . . . 20 (1 / 3) ∈ ℂ
28858, 87, 287mul32i 11457 . . . . . . . . . . . . . . . . . . 19 ((3 · 2) · (1 / 3)) = ((3 · (1 / 3)) · 2)
28958, 184recidi 11998 . . . . . . . . . . . . . . . . . . . . 21 (3 · (1 / 3)) = 1
290289oveq1i 7441 . . . . . . . . . . . . . . . . . . . 20 ((3 · (1 / 3)) · 2) = (1 · 2)
29187mullidi 11266 . . . . . . . . . . . . . . . . . . . 20 (1 · 2) = 2
292290, 291eqtri 2765 . . . . . . . . . . . . . . . . . . 19 ((3 · (1 / 3)) · 2) = 2
293288, 292eqtri 2765 . . . . . . . . . . . . . . . . . 18 ((3 · 2) · (1 / 3)) = 2
294187, 178eqeltri 2837 . . . . . . . . . . . . . . . . . . 19 (3 · 2) ∈ ℂ
295187, 249eqnetri 3011 . . . . . . . . . . . . . . . . . . 19 (3 · 2) ≠ 0
29687, 294, 287, 295divmuli 12021 . . . . . . . . . . . . . . . . . 18 ((2 / (3 · 2)) = (1 / 3) ↔ ((3 · 2) · (1 / 3)) = 2)
297293, 296mpbir 231 . . . . . . . . . . . . . . . . 17 (2 / (3 · 2)) = (1 / 3)
29887, 178, 249divreci 12012 . . . . . . . . . . . . . . . . 17 (2 / 6) = (2 · (1 / 6))
299286, 297, 2983eqtr3ri 2774 . . . . . . . . . . . . . . . 16 (2 · (1 / 6)) = (1 / 3)
300299a1i 11 . . . . . . . . . . . . . . 15 (𝑋 ∈ ℂ → (2 · (1 / 6)) = (1 / 3))
301285, 300oveq12d 7449 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → ((2 · ((𝑋↑2) − 𝑋)) + (2 · (1 / 6))) = (((2 · (𝑋↑2)) − (2 · 𝑋)) + (1 / 3)))
302284, 301eqtrd 2777 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (2 · (((𝑋↑2) − 𝑋) + (1 / 6))) = (((2 · (𝑋↑2)) − (2 · 𝑋)) + (1 / 3)))
303302oveq2d 7447 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → (𝑋 + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))) = (𝑋 + (((2 · (𝑋↑2)) − (2 · 𝑋)) + (1 / 3))))
304191, 224mulcld 11281 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → (2 · (𝑋↑2)) ∈ ℂ)
305191, 242mulcld 11281 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → (2 · 𝑋) ∈ ℂ)
306304, 305subcld 11620 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → ((2 · (𝑋↑2)) − (2 · 𝑋)) ∈ ℂ)
307287a1i 11 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (1 / 3) ∈ ℂ)
308242, 306, 307addassd 11283 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → ((𝑋 + ((2 · (𝑋↑2)) − (2 · 𝑋))) + (1 / 3)) = (𝑋 + (((2 · (𝑋↑2)) − (2 · 𝑋)) + (1 / 3))))
309242, 304, 305addsub12d 11643 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (𝑋 + ((2 · (𝑋↑2)) − (2 · 𝑋))) = ((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))))
310309oveq1d 7446 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → ((𝑋 + ((2 · (𝑋↑2)) − (2 · 𝑋))) + (1 / 3)) = (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3)))
311303, 308, 3103eqtr2d 2783 . . . . . . . . . . 11 (𝑋 ∈ ℂ → (𝑋 + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))) = (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3)))
312311oveq2d 7447 . . . . . . . . . 10 (𝑋 ∈ ℂ → (((1 / 5) + (𝑋 − (1 / 2))) + (𝑋 + (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))) = (((1 / 5) + (𝑋 − (1 / 2))) + (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3))))
313283, 312eqtrd 2777 . . . . . . . . 9 (𝑋 ∈ ℂ → (𝑋 + (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))) = (((1 / 5) + (𝑋 − (1 / 2))) + (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3))))
314313oveq2d 7447 . . . . . . . 8 (𝑋 ∈ ℂ → ((3 · (𝑋↑2)) − (𝑋 + (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))))) = ((3 · (𝑋↑2)) − (((1 / 5) + (𝑋 − (1 / 2))) + (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3)))))
315242, 305subcld 11620 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (𝑋 − (2 · 𝑋)) ∈ ℂ)
316304, 315addcld 11280 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → ((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) ∈ ℂ)
317241, 245, 316, 307add4d 11490 . . . . . . . . . . 11 (𝑋 ∈ ℂ → (((1 / 5) + (𝑋 − (1 / 2))) + (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3))) = (((1 / 5) + ((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋)))) + ((𝑋 − (1 / 2)) + (1 / 3))))
318241, 304, 315add12d 11488 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → ((1 / 5) + ((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋)))) = ((2 · (𝑋↑2)) + ((1 / 5) + (𝑋 − (2 · 𝑋)))))
319318oveq1d 7446 . . . . . . . . . . 11 (𝑋 ∈ ℂ → (((1 / 5) + ((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋)))) + ((𝑋 − (1 / 2)) + (1 / 3))) = (((2 · (𝑋↑2)) + ((1 / 5) + (𝑋 − (2 · 𝑋)))) + ((𝑋 − (1 / 2)) + (1 / 3))))
320241, 315addcld 11280 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → ((1 / 5) + (𝑋 − (2 · 𝑋))) ∈ ℂ)
321245, 307addcld 11280 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → ((𝑋 − (1 / 2)) + (1 / 3)) ∈ ℂ)
322304, 320, 321addassd 11283 . . . . . . . . . . 11 (𝑋 ∈ ℂ → (((2 · (𝑋↑2)) + ((1 / 5) + (𝑋 − (2 · 𝑋)))) + ((𝑋 − (1 / 2)) + (1 / 3))) = ((2 · (𝑋↑2)) + (((1 / 5) + (𝑋 − (2 · 𝑋))) + ((𝑋 − (1 / 2)) + (1 / 3)))))
323317, 319, 3223eqtrd 2781 . . . . . . . . . 10 (𝑋 ∈ ℂ → (((1 / 5) + (𝑋 − (1 / 2))) + (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3))) = ((2 · (𝑋↑2)) + (((1 / 5) + (𝑋 − (2 · 𝑋))) + ((𝑋 − (1 / 2)) + (1 / 3)))))
324323oveq2d 7447 . . . . . . . . 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 11281 . . . . . . . . . 10 (𝑋 ∈ ℂ → (3 · (𝑋↑2)) ∈ ℂ)
326320, 321addcld 11280 . . . . . . . . . 10 (𝑋 ∈ ℂ → (((1 / 5) + (𝑋 − (2 · 𝑋))) + ((𝑋 − (1 / 2)) + (1 / 3))) ∈ ℂ)
327325, 304, 326subsub4d 11651 . . . . . . . . 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 11598 . . . . . . . . . . . 12 (3 − 2) = 1
329328oveq1i 7441 . . . . . . . . . . 11 ((3 − 2) · (𝑋↑2)) = (1 · (𝑋↑2))
330183, 191, 224subdird 11720 . . . . . . . . . . 11 (𝑋 ∈ ℂ → ((3 − 2) · (𝑋↑2)) = ((3 · (𝑋↑2)) − (2 · (𝑋↑2))))
331224mullidd 11279 . . . . . . . . . . 11 (𝑋 ∈ ℂ → (1 · (𝑋↑2)) = (𝑋↑2))
332329, 330, 3313eqtr3a 2801 . . . . . . . . . 10 (𝑋 ∈ ℂ → ((3 · (𝑋↑2)) − (2 · (𝑋↑2))) = (𝑋↑2))
333241, 305, 242subsubd 11648 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → ((1 / 5) − ((2 · 𝑋) − 𝑋)) = (((1 / 5) − (2 · 𝑋)) + 𝑋))
334 2txmxeqx 12406 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → ((2 · 𝑋) − 𝑋) = 𝑋)
335334oveq2d 7447 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → ((1 / 5) − ((2 · 𝑋) − 𝑋)) = ((1 / 5) − 𝑋))
336241, 305, 242subadd23d 11642 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (((1 / 5) − (2 · 𝑋)) + 𝑋) = ((1 / 5) + (𝑋 − (2 · 𝑋))))
337333, 335, 3363eqtr3d 2785 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → ((1 / 5) − 𝑋) = ((1 / 5) + (𝑋 − (2 · 𝑋))))
338242, 244, 307subsubd 11648 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → (𝑋 − ((1 / 2) − (1 / 3))) = ((𝑋 − (1 / 2)) + (1 / 3)))
339337, 338oveq12d 7449 . . . . . . . . . . 11 (𝑋 ∈ ℂ → (((1 / 5) − 𝑋) + (𝑋 − ((1 / 2) − (1 / 3)))) = (((1 / 5) + (𝑋 − (2 · 𝑋))) + ((𝑋 − (1 / 2)) + (1 / 3))))
340243, 287subcli 11585 . . . . . . . . . . . . . 14 ((1 / 2) − (1 / 3)) ∈ ℂ
341340a1i 11 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → ((1 / 2) − (1 / 3)) ∈ ℂ)
342241, 242, 341npncand 11644 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → (((1 / 5) − 𝑋) + (𝑋 − ((1 / 2) − (1 / 3)))) = ((1 / 5) − ((1 / 2) − (1 / 3))))
343 halfthird 12876 . . . . . . . . . . . . . 14 ((1 / 2) − (1 / 3)) = (1 / 6)
344343oveq2i 7442 . . . . . . . . . . . . 13 ((1 / 5) − ((1 / 2) − (1 / 3))) = ((1 / 5) − (1 / 6))
345 5recm6rec 12877 . . . . . . . . . . . . 13 ((1 / 5) − (1 / 6)) = (1 / 30)
346344, 345eqtri 2765 . . . . . . . . . . . 12 ((1 / 5) − ((1 / 2) − (1 / 3))) = (1 / 30)
347342, 346eqtrdi 2793 . . . . . . . . . . 11 (𝑋 ∈ ℂ → (((1 / 5) − 𝑋) + (𝑋 − ((1 / 2) − (1 / 3)))) = (1 / 30))
348339, 347eqtr3d 2779 . . . . . . . . . 10 (𝑋 ∈ ℂ → (((1 / 5) + (𝑋 − (2 · 𝑋))) + ((𝑋 − (1 / 2)) + (1 / 3))) = (1 / 30))
349332, 348oveq12d 7449 . . . . . . . . 9 (𝑋 ∈ ℂ → (((3 · (𝑋↑2)) − (2 · (𝑋↑2))) − (((1 / 5) + (𝑋 − (2 · 𝑋))) + ((𝑋 − (1 / 2)) + (1 / 3)))) = ((𝑋↑2) − (1 / 30)))
350324, 327, 3493eqtr2d 2783 . . . . . . . 8 (𝑋 ∈ ℂ → ((3 · (𝑋↑2)) − (((1 / 5) + (𝑋 − (1 / 2))) + (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3)))) = ((𝑋↑2) − (1 / 30)))
351282, 314, 3503eqtrd 2781 . . . . . . 7 (𝑋 ∈ ℂ → ((2 · ((3 / 2) · (𝑋↑2))) − (𝑋 + (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))))) = ((𝑋↑2) − (1 / 30)))
352351oveq2d 7447 . . . . . 6 (𝑋 ∈ ℂ → ((2 · (𝑋↑3)) − ((2 · ((3 / 2) · (𝑋↑2))) − (𝑋 + (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))))) = ((2 · (𝑋↑3)) − ((𝑋↑2) − (1 / 30))))
353275, 277, 3523eqtr2d 2783 . . . . 5 (𝑋 ∈ ℂ → ((((2 · (𝑋↑3)) − (2 · ((3 / 2) · (𝑋↑2)))) + 𝑋) + (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))) = ((2 · (𝑋↑3)) − ((𝑋↑2) − (1 / 30))))
354262, 272, 3533eqtrd 2781 . . . 4 (𝑋 ∈ ℂ → ((((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))) + (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋)))) = ((2 · (𝑋↑3)) − ((𝑋↑2) − (1 / 30))))
355354oveq2d 7447 . . 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 11620 . . . 4 (𝑋 ∈ ℂ → ((𝑋↑4) − (2 · (𝑋↑3))) ∈ ℂ)
357356, 224, 238addsubassd 11640 . . 3 (𝑋 ∈ ℂ → ((((𝑋↑4) − (2 · (𝑋↑3))) + (𝑋↑2)) − (1 / 30)) = (((𝑋↑4) − (2 · (𝑋↑3))) + ((𝑋↑2) − (1 / 30))))
358240, 355, 3573eqtr4d 2787 . 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 2781 1 (𝑋 ∈ ℂ → (4 BernPoly 𝑋) = ((((𝑋↑4) − (2 · (𝑋↑3))) + (𝑋↑2)) − (1 / 30)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1540  wcel 2108  wne 2940  wss 3951   class class class wbr 5143  cfv 6561  (class class class)co 7431  cc 11153  cr 11154  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160   < clt 11295  cmin 11492   / cdiv 11920  cn 12266  2c2 12321  3c3 12322  4c4 12323  5c5 12324  6c6 12325  0cn0 12526  cz 12613  cdc 12733  cuz 12878  ...cfz 13547  cexp 14102  Ccbc 14341  Σcsu 15722   BernPoly cbp 16082
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-sup 9482  df-oi 9550  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336  df-n0 12527  df-z 12614  df-dec 12734  df-uz 12879  df-rp 13035  df-fz 13548  df-fzo 13695  df-seq 14043  df-exp 14103  df-fac 14313  df-bc 14342  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-clim 15524  df-sum 15723  df-bpoly 16083
This theorem is referenced by:  fsumcube  16096
  Copyright terms: Public domain W3C validator