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

Theorem bpoly4 15403
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 11905 . . 3 4 ∈ ℕ0
2 bpolyval 15393 . . 3 ((4 ∈ ℕ0𝑋 ∈ ℂ) → (4 BernPoly 𝑋) = ((𝑋↑4) − Σ𝑘 ∈ (0...(4 − 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)))))
31, 2mpan 686 . 2 (𝑋 ∈ ℂ → (4 BernPoly 𝑋) = ((𝑋↑4) − Σ𝑘 ∈ (0...(4 − 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)))))
4 4m1e3 11755 . . . . . . 7 (4 − 1) = 3
5 df-3 11690 . . . . . . 7 3 = (2 + 1)
64, 5eqtri 2844 . . . . . 6 (4 − 1) = (2 + 1)
76oveq2i 7156 . . . . 5 (0...(4 − 1)) = (0...(2 + 1))
87sumeq1i 15045 . . . 4 Σ𝑘 ∈ (0...(4 − 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = Σ𝑘 ∈ (0...(2 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)))
9 2eluzge0 12282 . . . . . . 7 2 ∈ (ℤ‘0)
109a1i 11 . . . . . 6 (𝑋 ∈ ℂ → 2 ∈ (ℤ‘0))
11 elfzelz 12898 . . . . . . . . . 10 (𝑘 ∈ (0...(2 + 1)) → 𝑘 ∈ ℤ)
12 bccl 13672 . . . . . . . . . 10 ((4 ∈ ℕ0𝑘 ∈ ℤ) → (4C𝑘) ∈ ℕ0)
131, 11, 12sylancr 587 . . . . . . . . 9 (𝑘 ∈ (0...(2 + 1)) → (4C𝑘) ∈ ℕ0)
1413nn0cnd 11946 . . . . . . . 8 (𝑘 ∈ (0...(2 + 1)) → (4C𝑘) ∈ ℂ)
1514adantl 482 . . . . . . 7 ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(2 + 1))) → (4C𝑘) ∈ ℂ)
16 elfznn0 12990 . . . . . . . . . 10 (𝑘 ∈ (0...(2 + 1)) → 𝑘 ∈ ℕ0)
17 bpolycl 15396 . . . . . . . . . 10 ((𝑘 ∈ ℕ0𝑋 ∈ ℂ) → (𝑘 BernPoly 𝑋) ∈ ℂ)
1816, 17sylan 580 . . . . . . . . 9 ((𝑘 ∈ (0...(2 + 1)) ∧ 𝑋 ∈ ℂ) → (𝑘 BernPoly 𝑋) ∈ ℂ)
1918ancoms 459 . . . . . . . 8 ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(2 + 1))) → (𝑘 BernPoly 𝑋) ∈ ℂ)
20 4re 11710 . . . . . . . . . . . . 13 4 ∈ ℝ
2120a1i 11 . . . . . . . . . . . 12 (𝑘 ∈ (0...(2 + 1)) → 4 ∈ ℝ)
2211zred 12076 . . . . . . . . . . . 12 (𝑘 ∈ (0...(2 + 1)) → 𝑘 ∈ ℝ)
2321, 22resubcld 11057 . . . . . . . . . . 11 (𝑘 ∈ (0...(2 + 1)) → (4 − 𝑘) ∈ ℝ)
24 peano2re 10802 . . . . . . . . . . 11 ((4 − 𝑘) ∈ ℝ → ((4 − 𝑘) + 1) ∈ ℝ)
2523, 24syl 17 . . . . . . . . . 10 (𝑘 ∈ (0...(2 + 1)) → ((4 − 𝑘) + 1) ∈ ℝ)
2625recnd 10658 . . . . . . . . 9 (𝑘 ∈ (0...(2 + 1)) → ((4 − 𝑘) + 1) ∈ ℂ)
2726adantl 482 . . . . . . . 8 ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(2 + 1))) → ((4 − 𝑘) + 1) ∈ ℂ)
28 1red 10631 . . . . . . . . . . 11 (𝑘 ∈ (0...(2 + 1)) → 1 ∈ ℝ)
295oveq2i 7156 . . . . . . . . . . . . . 14 (0...3) = (0...(2 + 1))
3029eleq2i 2904 . . . . . . . . . . . . 13 (𝑘 ∈ (0...3) ↔ 𝑘 ∈ (0...(2 + 1)))
31 elfzelz 12898 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...3) → 𝑘 ∈ ℤ)
3231zred 12076 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...3) → 𝑘 ∈ ℝ)
33 3re 11706 . . . . . . . . . . . . . . 15 3 ∈ ℝ
3433a1i 11 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...3) → 3 ∈ ℝ)
3520a1i 11 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...3) → 4 ∈ ℝ)
36 elfzle2 12901 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...3) → 𝑘 ≤ 3)
37 3lt4 11800 . . . . . . . . . . . . . . 15 3 < 4
3837a1i 11 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...3) → 3 < 4)
3932, 34, 35, 36, 38lelttrd 10787 . . . . . . . . . . . . 13 (𝑘 ∈ (0...3) → 𝑘 < 4)
4030, 39sylbir 236 . . . . . . . . . . . 12 (𝑘 ∈ (0...(2 + 1)) → 𝑘 < 4)
4122, 21posdifd 11216 . . . . . . . . . . . 12 (𝑘 ∈ (0...(2 + 1)) → (𝑘 < 4 ↔ 0 < (4 − 𝑘)))
4240, 41mpbid 233 . . . . . . . . . . 11 (𝑘 ∈ (0...(2 + 1)) → 0 < (4 − 𝑘))
43 0lt1 11151 . . . . . . . . . . . 12 0 < 1
4443a1i 11 . . . . . . . . . . 11 (𝑘 ∈ (0...(2 + 1)) → 0 < 1)
4523, 28, 42, 44addgt0d 11204 . . . . . . . . . 10 (𝑘 ∈ (0...(2 + 1)) → 0 < ((4 − 𝑘) + 1))
4645gt0ne0d 11193 . . . . . . . . 9 (𝑘 ∈ (0...(2 + 1)) → ((4 − 𝑘) + 1) ≠ 0)
4746adantl 482 . . . . . . . 8 ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(2 + 1))) → ((4 − 𝑘) + 1) ≠ 0)
4819, 27, 47divcld 11405 . . . . . . 7 ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(2 + 1))) → ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)) ∈ ℂ)
4915, 48mulcld 10650 . . . . . 6 ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(2 + 1))) → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) ∈ ℂ)
505eqeq2i 2834 . . . . . . 7 (𝑘 = 3 ↔ 𝑘 = (2 + 1))
51 oveq2 7153 . . . . . . . . 9 (𝑘 = 3 → (4C𝑘) = (4C3))
52 4bc3eq4 13678 . . . . . . . . 9 (4C3) = 4
5351, 52syl6eq 2872 . . . . . . . 8 (𝑘 = 3 → (4C𝑘) = 4)
54 oveq1 7152 . . . . . . . . 9 (𝑘 = 3 → (𝑘 BernPoly 𝑋) = (3 BernPoly 𝑋))
55 oveq2 7153 . . . . . . . . . . 11 (𝑘 = 3 → (4 − 𝑘) = (4 − 3))
5655oveq1d 7160 . . . . . . . . . 10 (𝑘 = 3 → ((4 − 𝑘) + 1) = ((4 − 3) + 1))
57 4cn 11711 . . . . . . . . . . . . 13 4 ∈ ℂ
58 3cn 11707 . . . . . . . . . . . . 13 3 ∈ ℂ
59 ax-1cn 10584 . . . . . . . . . . . . 13 1 ∈ ℂ
60 3p1e4 11771 . . . . . . . . . . . . 13 (3 + 1) = 4
6157, 58, 59, 60subaddrii 10964 . . . . . . . . . . . 12 (4 − 3) = 1
6261oveq1i 7155 . . . . . . . . . . 11 ((4 − 3) + 1) = (1 + 1)
63 df-2 11689 . . . . . . . . . . 11 2 = (1 + 1)
6462, 63eqtr4i 2847 . . . . . . . . . 10 ((4 − 3) + 1) = 2
6556, 64syl6eq 2872 . . . . . . . . 9 (𝑘 = 3 → ((4 − 𝑘) + 1) = 2)
6654, 65oveq12d 7163 . . . . . . . 8 (𝑘 = 3 → ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)) = ((3 BernPoly 𝑋) / 2))
6753, 66oveq12d 7163 . . . . . . 7 (𝑘 = 3 → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (4 · ((3 BernPoly 𝑋) / 2)))
6850, 67sylbir 236 . . . . . 6 (𝑘 = (2 + 1) → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (4 · ((3 BernPoly 𝑋) / 2)))
6910, 49, 68fsump1 15101 . . . . 5 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...(2 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (Σ𝑘 ∈ (0...2)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) + (4 · ((3 BernPoly 𝑋) / 2))))
7063oveq2i 7156 . . . . . . . 8 (0...2) = (0...(1 + 1))
7170sumeq1i 15045 . . . . . . 7 Σ𝑘 ∈ (0...2)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = Σ𝑘 ∈ (0...(1 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)))
72 1eluzge0 12281 . . . . . . . . . 10 1 ∈ (ℤ‘0)
7372a1i 11 . . . . . . . . 9 (𝑋 ∈ ℂ → 1 ∈ (ℤ‘0))
74 fzssp1 12940 . . . . . . . . . . . 12 (0...(1 + 1)) ⊆ (0...((1 + 1) + 1))
7563oveq1i 7155 . . . . . . . . . . . . 13 (2 + 1) = ((1 + 1) + 1)
7675oveq2i 7156 . . . . . . . . . . . 12 (0...(2 + 1)) = (0...((1 + 1) + 1))
7774, 76sseqtrri 4003 . . . . . . . . . . 11 (0...(1 + 1)) ⊆ (0...(2 + 1))
7877sseli 3962 . . . . . . . . . 10 (𝑘 ∈ (0...(1 + 1)) → 𝑘 ∈ (0...(2 + 1)))
7978, 49sylan2 592 . . . . . . . . 9 ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(1 + 1))) → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) ∈ ℂ)
8063eqeq2i 2834 . . . . . . . . . 10 (𝑘 = 2 ↔ 𝑘 = (1 + 1))
81 oveq2 7153 . . . . . . . . . . . 12 (𝑘 = 2 → (4C𝑘) = (4C2))
82 4bc2eq6 13679 . . . . . . . . . . . 12 (4C2) = 6
8381, 82syl6eq 2872 . . . . . . . . . . 11 (𝑘 = 2 → (4C𝑘) = 6)
84 oveq1 7152 . . . . . . . . . . . 12 (𝑘 = 2 → (𝑘 BernPoly 𝑋) = (2 BernPoly 𝑋))
85 oveq2 7153 . . . . . . . . . . . . . 14 (𝑘 = 2 → (4 − 𝑘) = (4 − 2))
8685oveq1d 7160 . . . . . . . . . . . . 13 (𝑘 = 2 → ((4 − 𝑘) + 1) = ((4 − 2) + 1))
87 2cn 11701 . . . . . . . . . . . . . . . 16 2 ∈ ℂ
88 2p2e4 11761 . . . . . . . . . . . . . . . 16 (2 + 2) = 4
8957, 87, 87, 88subaddrii 10964 . . . . . . . . . . . . . . 15 (4 − 2) = 2
9089oveq1i 7155 . . . . . . . . . . . . . 14 ((4 − 2) + 1) = (2 + 1)
9190, 5eqtr4i 2847 . . . . . . . . . . . . 13 ((4 − 2) + 1) = 3
9286, 91syl6eq 2872 . . . . . . . . . . . 12 (𝑘 = 2 → ((4 − 𝑘) + 1) = 3)
9384, 92oveq12d 7163 . . . . . . . . . . 11 (𝑘 = 2 → ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)) = ((2 BernPoly 𝑋) / 3))
9483, 93oveq12d 7163 . . . . . . . . . 10 (𝑘 = 2 → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (6 · ((2 BernPoly 𝑋) / 3)))
9580, 94sylbir 236 . . . . . . . . 9 (𝑘 = (1 + 1) → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (6 · ((2 BernPoly 𝑋) / 3)))
9673, 79, 95fsump1 15101 . . . . . . . 8 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...(1 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (Σ𝑘 ∈ (0...1)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) + (6 · ((2 BernPoly 𝑋) / 3))))
97 0p1e1 11748 . . . . . . . . . . . 12 (0 + 1) = 1
9897oveq2i 7156 . . . . . . . . . . 11 (0...(0 + 1)) = (0...1)
9998sumeq1i 15045 . . . . . . . . . 10 Σ𝑘 ∈ (0...(0 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = Σ𝑘 ∈ (0...1)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)))
100 0nn0 11901 . . . . . . . . . . . . . 14 0 ∈ ℕ0
101 nn0uz 12269 . . . . . . . . . . . . . 14 0 = (ℤ‘0)
102100, 101eleqtri 2911 . . . . . . . . . . . . 13 0 ∈ (ℤ‘0)
103102a1i 11 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → 0 ∈ (ℤ‘0))
104 3nn 11705 . . . . . . . . . . . . . . . . 17 3 ∈ ℕ
105 nnuz 12270 . . . . . . . . . . . . . . . . 17 ℕ = (ℤ‘1)
106104, 105eleqtri 2911 . . . . . . . . . . . . . . . 16 3 ∈ (ℤ‘1)
107 fzss2 12937 . . . . . . . . . . . . . . . 16 (3 ∈ (ℤ‘1) → (0...1) ⊆ (0...3))
108106, 107ax-mp 5 . . . . . . . . . . . . . . 15 (0...1) ⊆ (0...3)
109 2p1e3 11768 . . . . . . . . . . . . . . . 16 (2 + 1) = 3
110109oveq2i 7156 . . . . . . . . . . . . . . 15 (0...(2 + 1)) = (0...3)
111108, 98, 1103sstr4i 4009 . . . . . . . . . . . . . 14 (0...(0 + 1)) ⊆ (0...(2 + 1))
112111sseli 3962 . . . . . . . . . . . . 13 (𝑘 ∈ (0...(0 + 1)) → 𝑘 ∈ (0...(2 + 1)))
113112, 49sylan2 592 . . . . . . . . . . . 12 ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(0 + 1))) → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) ∈ ℂ)
11497eqeq2i 2834 . . . . . . . . . . . . 13 (𝑘 = (0 + 1) ↔ 𝑘 = 1)
115 oveq2 7153 . . . . . . . . . . . . . . 15 (𝑘 = 1 → (4C𝑘) = (4C1))
116 bcn1 13663 . . . . . . . . . . . . . . . 16 (4 ∈ ℕ0 → (4C1) = 4)
1171, 116ax-mp 5 . . . . . . . . . . . . . . 15 (4C1) = 4
118115, 117syl6eq 2872 . . . . . . . . . . . . . 14 (𝑘 = 1 → (4C𝑘) = 4)
119 oveq1 7152 . . . . . . . . . . . . . . 15 (𝑘 = 1 → (𝑘 BernPoly 𝑋) = (1 BernPoly 𝑋))
120 oveq2 7153 . . . . . . . . . . . . . . . . 17 (𝑘 = 1 → (4 − 𝑘) = (4 − 1))
121120oveq1d 7160 . . . . . . . . . . . . . . . 16 (𝑘 = 1 → ((4 − 𝑘) + 1) = ((4 − 1) + 1))
1224oveq1i 7155 . . . . . . . . . . . . . . . . 17 ((4 − 1) + 1) = (3 + 1)
123 df-4 11691 . . . . . . . . . . . . . . . . 17 4 = (3 + 1)
124122, 123eqtr4i 2847 . . . . . . . . . . . . . . . 16 ((4 − 1) + 1) = 4
125121, 124syl6eq 2872 . . . . . . . . . . . . . . 15 (𝑘 = 1 → ((4 − 𝑘) + 1) = 4)
126119, 125oveq12d 7163 . . . . . . . . . . . . . 14 (𝑘 = 1 → ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)) = ((1 BernPoly 𝑋) / 4))
127118, 126oveq12d 7163 . . . . . . . . . . . . 13 (𝑘 = 1 → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (4 · ((1 BernPoly 𝑋) / 4)))
128114, 127sylbi 218 . . . . . . . . . . . 12 (𝑘 = (0 + 1) → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (4 · ((1 BernPoly 𝑋) / 4)))
129103, 113, 128fsump1 15101 . . . . . . . . . . 11 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...(0 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (Σ𝑘 ∈ (0...0)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) + (4 · ((1 BernPoly 𝑋) / 4))))
130 0z 11981 . . . . . . . . . . . . . 14 0 ∈ ℤ
13159a1i 11 . . . . . . . . . . . . . . 15 (𝑋 ∈ ℂ → 1 ∈ ℂ)
132 bpolycl 15396 . . . . . . . . . . . . . . . . 17 ((0 ∈ ℕ0𝑋 ∈ ℂ) → (0 BernPoly 𝑋) ∈ ℂ)
133100, 132mpan 686 . . . . . . . . . . . . . . . 16 (𝑋 ∈ ℂ → (0 BernPoly 𝑋) ∈ ℂ)
134 5cn 11714 . . . . . . . . . . . . . . . . 17 5 ∈ ℂ
135134a1i 11 . . . . . . . . . . . . . . . 16 (𝑋 ∈ ℂ → 5 ∈ ℂ)
136 0re 10632 . . . . . . . . . . . . . . . . . 18 0 ∈ ℝ
137 5pos 11735 . . . . . . . . . . . . . . . . . 18 0 < 5
138136, 137gtneii 10741 . . . . . . . . . . . . . . . . 17 5 ≠ 0
139138a1i 11 . . . . . . . . . . . . . . . 16 (𝑋 ∈ ℂ → 5 ≠ 0)
140133, 135, 139divcld 11405 . . . . . . . . . . . . . . 15 (𝑋 ∈ ℂ → ((0 BernPoly 𝑋) / 5) ∈ ℂ)
141131, 140mulcld 10650 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → (1 · ((0 BernPoly 𝑋) / 5)) ∈ ℂ)
142 oveq2 7153 . . . . . . . . . . . . . . . . 17 (𝑘 = 0 → (4C𝑘) = (4C0))
143 bcn0 13660 . . . . . . . . . . . . . . . . . 18 (4 ∈ ℕ0 → (4C0) = 1)
1441, 143ax-mp 5 . . . . . . . . . . . . . . . . 17 (4C0) = 1
145142, 144syl6eq 2872 . . . . . . . . . . . . . . . 16 (𝑘 = 0 → (4C𝑘) = 1)
146 oveq1 7152 . . . . . . . . . . . . . . . . 17 (𝑘 = 0 → (𝑘 BernPoly 𝑋) = (0 BernPoly 𝑋))
147 oveq2 7153 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 0 → (4 − 𝑘) = (4 − 0))
148147oveq1d 7160 . . . . . . . . . . . . . . . . . 18 (𝑘 = 0 → ((4 − 𝑘) + 1) = ((4 − 0) + 1))
14957subid1i 10947 . . . . . . . . . . . . . . . . . . . 20 (4 − 0) = 4
150149oveq1i 7155 . . . . . . . . . . . . . . . . . . 19 ((4 − 0) + 1) = (4 + 1)
151 4p1e5 11772 . . . . . . . . . . . . . . . . . . 19 (4 + 1) = 5
152150, 151eqtri 2844 . . . . . . . . . . . . . . . . . 18 ((4 − 0) + 1) = 5
153148, 152syl6eq 2872 . . . . . . . . . . . . . . . . 17 (𝑘 = 0 → ((4 − 𝑘) + 1) = 5)
154146, 153oveq12d 7163 . . . . . . . . . . . . . . . 16 (𝑘 = 0 → ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)) = ((0 BernPoly 𝑋) / 5))
155145, 154oveq12d 7163 . . . . . . . . . . . . . . 15 (𝑘 = 0 → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (1 · ((0 BernPoly 𝑋) / 5)))
156155fsum1 15092 . . . . . . . . . . . . . 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 15394 . . . . . . . . . . . . . . . 16 (𝑋 ∈ ℂ → (0 BernPoly 𝑋) = 1)
159158oveq1d 7160 . . . . . . . . . . . . . . 15 (𝑋 ∈ ℂ → ((0 BernPoly 𝑋) / 5) = (1 / 5))
160159oveq2d 7161 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → (1 · ((0 BernPoly 𝑋) / 5)) = (1 · (1 / 5)))
161134, 138reccli 11359 . . . . . . . . . . . . . . 15 (1 / 5) ∈ ℂ
162161mulid2i 10635 . . . . . . . . . . . . . 14 (1 · (1 / 5)) = (1 / 5)
163160, 162syl6eq 2872 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (1 · ((0 BernPoly 𝑋) / 5)) = (1 / 5))
164157, 163eqtrd 2856 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...0)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (1 / 5))
165 1nn0 11902 . . . . . . . . . . . . . . 15 1 ∈ ℕ0
166 bpolycl 15396 . . . . . . . . . . . . . . 15 ((1 ∈ ℕ0𝑋 ∈ ℂ) → (1 BernPoly 𝑋) ∈ ℂ)
167165, 166mpan 686 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → (1 BernPoly 𝑋) ∈ ℂ)
168 nn0cn 11896 . . . . . . . . . . . . . . 15 (4 ∈ ℕ0 → 4 ∈ ℂ)
1691, 168mp1i 13 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → 4 ∈ ℂ)
170 4ne0 11734 . . . . . . . . . . . . . . 15 4 ≠ 0
171170a1i 11 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → 4 ≠ 0)
172167, 169, 171divcan2d 11407 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (4 · ((1 BernPoly 𝑋) / 4)) = (1 BernPoly 𝑋))
173 bpoly1 15395 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (1 BernPoly 𝑋) = (𝑋 − (1 / 2)))
174172, 173eqtrd 2856 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → (4 · ((1 BernPoly 𝑋) / 4)) = (𝑋 − (1 / 2)))
175164, 174oveq12d 7163 . . . . . . . . . . 11 (𝑋 ∈ ℂ → (Σ𝑘 ∈ (0...0)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) + (4 · ((1 BernPoly 𝑋) / 4))) = ((1 / 5) + (𝑋 − (1 / 2))))
176129, 175eqtrd 2856 . . . . . . . . . 10 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...(0 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = ((1 / 5) + (𝑋 − (1 / 2))))
17799, 176syl5eqr 2870 . . . . . . . . 9 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...1)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = ((1 / 5) + (𝑋 − (1 / 2))))
178 6cn 11717 . . . . . . . . . . . 12 6 ∈ ℂ
179178a1i 11 . . . . . . . . . . 11 (𝑋 ∈ ℂ → 6 ∈ ℂ)
180 2nn0 11903 . . . . . . . . . . . 12 2 ∈ ℕ0
181 bpolycl 15396 . . . . . . . . . . . 12 ((2 ∈ ℕ0𝑋 ∈ ℂ) → (2 BernPoly 𝑋) ∈ ℂ)
182180, 181mpan 686 . . . . . . . . . . 11 (𝑋 ∈ ℂ → (2 BernPoly 𝑋) ∈ ℂ)
18358a1i 11 . . . . . . . . . . 11 (𝑋 ∈ ℂ → 3 ∈ ℂ)
184 3ne0 11732 . . . . . . . . . . . 12 3 ≠ 0
185184a1i 11 . . . . . . . . . . 11 (𝑋 ∈ ℂ → 3 ≠ 0)
186179, 182, 183, 185div12d 11441 . . . . . . . . . 10 (𝑋 ∈ ℂ → (6 · ((2 BernPoly 𝑋) / 3)) = ((2 BernPoly 𝑋) · (6 / 3)))
187 3t2e6 11792 . . . . . . . . . . . . 13 (3 · 2) = 6
188178, 58, 87, 184divmuli 11383 . . . . . . . . . . . . 13 ((6 / 3) = 2 ↔ (3 · 2) = 6)
189187, 188mpbir 232 . . . . . . . . . . . 12 (6 / 3) = 2
190189oveq2i 7156 . . . . . . . . . . 11 ((2 BernPoly 𝑋) · (6 / 3)) = ((2 BernPoly 𝑋) · 2)
19187a1i 11 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → 2 ∈ ℂ)
192182, 191mulcomd 10651 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → ((2 BernPoly 𝑋) · 2) = (2 · (2 BernPoly 𝑋)))
193 bpoly2 15401 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (2 BernPoly 𝑋) = (((𝑋↑2) − 𝑋) + (1 / 6)))
194193oveq2d 7161 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → (2 · (2 BernPoly 𝑋)) = (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))
195192, 194eqtrd 2856 . . . . . . . . . . 11 (𝑋 ∈ ℂ → ((2 BernPoly 𝑋) · 2) = (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))
196190, 195syl5eq 2868 . . . . . . . . . 10 (𝑋 ∈ ℂ → ((2 BernPoly 𝑋) · (6 / 3)) = (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))
197186, 196eqtrd 2856 . . . . . . . . 9 (𝑋 ∈ ℂ → (6 · ((2 BernPoly 𝑋) / 3)) = (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))
198177, 197oveq12d 7163 . . . . . . . 8 (𝑋 ∈ ℂ → (Σ𝑘 ∈ (0...1)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) + (6 · ((2 BernPoly 𝑋) / 3))) = (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))))
19996, 198eqtrd 2856 . . . . . . 7 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...(1 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))))
20071, 199syl5eq 2868 . . . . . 6 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...2)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))))
201 3nn0 11904 . . . . . . . . 9 3 ∈ ℕ0
202 bpolycl 15396 . . . . . . . . 9 ((3 ∈ ℕ0𝑋 ∈ ℂ) → (3 BernPoly 𝑋) ∈ ℂ)
203201, 202mpan 686 . . . . . . . 8 (𝑋 ∈ ℂ → (3 BernPoly 𝑋) ∈ ℂ)
204 2ne0 11730 . . . . . . . . 9 2 ≠ 0
205204a1i 11 . . . . . . . 8 (𝑋 ∈ ℂ → 2 ≠ 0)
206169, 203, 191, 205div12d 11441 . . . . . . 7 (𝑋 ∈ ℂ → (4 · ((3 BernPoly 𝑋) / 2)) = ((3 BernPoly 𝑋) · (4 / 2)))
207 4d2e2 11796 . . . . . . . . 9 (4 / 2) = 2
208207oveq2i 7156 . . . . . . . 8 ((3 BernPoly 𝑋) · (4 / 2)) = ((3 BernPoly 𝑋) · 2)
209203, 191mulcomd 10651 . . . . . . . . 9 (𝑋 ∈ ℂ → ((3 BernPoly 𝑋) · 2) = (2 · (3 BernPoly 𝑋)))
210 bpoly3 15402 . . . . . . . . . 10 (𝑋 ∈ ℂ → (3 BernPoly 𝑋) = (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋)))
211210oveq2d 7161 . . . . . . . . 9 (𝑋 ∈ ℂ → (2 · (3 BernPoly 𝑋)) = (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))))
212209, 211eqtrd 2856 . . . . . . . 8 (𝑋 ∈ ℂ → ((3 BernPoly 𝑋) · 2) = (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))))
213208, 212syl5eq 2868 . . . . . . 7 (𝑋 ∈ ℂ → ((3 BernPoly 𝑋) · (4 / 2)) = (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))))
214206, 213eqtrd 2856 . . . . . 6 (𝑋 ∈ ℂ → (4 · ((3 BernPoly 𝑋) / 2)) = (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))))
215200, 214oveq12d 7163 . . . . 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 2856 . . . 4 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...(2 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = ((((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))) + (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋)))))
2178, 216syl5eq 2868 . . 3 (𝑋 ∈ ℂ → Σ𝑘 ∈ (0...(4 − 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = ((((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))) + (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋)))))
218217oveq2d 7161 . 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 13437 . . . . 5 ((𝑋 ∈ ℂ ∧ 4 ∈ ℕ0) → (𝑋↑4) ∈ ℂ)
2201, 219mpan2 687 . . . 4 (𝑋 ∈ ℂ → (𝑋↑4) ∈ ℂ)
221 expcl 13437 . . . . . 6 ((𝑋 ∈ ℂ ∧ 3 ∈ ℕ0) → (𝑋↑3) ∈ ℂ)
222201, 221mpan2 687 . . . . 5 (𝑋 ∈ ℂ → (𝑋↑3) ∈ ℂ)
223191, 222mulcld 10650 . . . 4 (𝑋 ∈ ℂ → (2 · (𝑋↑3)) ∈ ℂ)
224 sqcl 13474 . . . . 5 (𝑋 ∈ ℂ → (𝑋↑2) ∈ ℂ)
225201, 100deccl 12102 . . . . . . . 8 30 ∈ ℕ0
226225nn0cni 11898 . . . . . . 7 30 ∈ ℂ
227 dfdec10 12090 . . . . . . . . 9 30 = ((10 · 3) + 0)
228 10re 12106 . . . . . . . . . . . 12 10 ∈ ℝ
229228recni 10644 . . . . . . . . . . 11 10 ∈ ℂ
230229, 58mulcli 10637 . . . . . . . . . 10 (10 · 3) ∈ ℂ
231230addid1i 10816 . . . . . . . . 9 ((10 · 3) + 0) = (10 · 3)
232227, 231eqtri 2844 . . . . . . . 8 30 = (10 · 3)
233 10pos 12104 . . . . . . . . . 10 0 < 10
234136, 233gtneii 10741 . . . . . . . . 9 10 ≠ 0
235229, 58, 234, 184mulne0i 11272 . . . . . . . 8 (10 · 3) ≠ 0
236232, 235eqnetri 3086 . . . . . . 7 30 ≠ 0
237226, 236reccli 11359 . . . . . 6 (1 / 30) ∈ ℂ
238237a1i 11 . . . . 5 (𝑋 ∈ ℂ → (1 / 30) ∈ ℂ)
239224, 238subcld 10986 . . . 4 (𝑋 ∈ ℂ → ((𝑋↑2) − (1 / 30)) ∈ ℂ)
240220, 223, 239subsubd 11014 . . 3 (𝑋 ∈ ℂ → ((𝑋↑4) − ((2 · (𝑋↑3)) − ((𝑋↑2) − (1 / 30)))) = (((𝑋↑4) − (2 · (𝑋↑3))) + ((𝑋↑2) − (1 / 30))))
241161a1i 11 . . . . . . . 8 (𝑋 ∈ ℂ → (1 / 5) ∈ ℂ)
242 id 22 . . . . . . . . 9 (𝑋 ∈ ℂ → 𝑋 ∈ ℂ)
24387, 204reccli 11359 . . . . . . . . . 10 (1 / 2) ∈ ℂ
244243a1i 11 . . . . . . . . 9 (𝑋 ∈ ℂ → (1 / 2) ∈ ℂ)
245242, 244subcld 10986 . . . . . . . 8 (𝑋 ∈ ℂ → (𝑋 − (1 / 2)) ∈ ℂ)
246241, 245addcld 10649 . . . . . . 7 (𝑋 ∈ ℂ → ((1 / 5) + (𝑋 − (1 / 2))) ∈ ℂ)
247224, 242subcld 10986 . . . . . . . . 9 (𝑋 ∈ ℂ → ((𝑋↑2) − 𝑋) ∈ ℂ)
248 6pos 11736 . . . . . . . . . . . 12 0 < 6
249136, 248gtneii 10741 . . . . . . . . . . 11 6 ≠ 0
250178, 249reccli 11359 . . . . . . . . . 10 (1 / 6) ∈ ℂ
251250a1i 11 . . . . . . . . 9 (𝑋 ∈ ℂ → (1 / 6) ∈ ℂ)
252247, 251addcld 10649 . . . . . . . 8 (𝑋 ∈ ℂ → (((𝑋↑2) − 𝑋) + (1 / 6)) ∈ ℂ)
253191, 252mulcld 10650 . . . . . . 7 (𝑋 ∈ ℂ → (2 · (((𝑋↑2) − 𝑋) + (1 / 6))) ∈ ℂ)
254246, 253addcld 10649 . . . . . 6 (𝑋 ∈ ℂ → (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))) ∈ ℂ)
25558, 87, 204divcli 11371 . . . . . . . . . . 11 (3 / 2) ∈ ℂ
256255a1i 11 . . . . . . . . . 10 (𝑋 ∈ ℂ → (3 / 2) ∈ ℂ)
257256, 224mulcld 10650 . . . . . . . . 9 (𝑋 ∈ ℂ → ((3 / 2) · (𝑋↑2)) ∈ ℂ)
258222, 257subcld 10986 . . . . . . . 8 (𝑋 ∈ ℂ → ((𝑋↑3) − ((3 / 2) · (𝑋↑2))) ∈ ℂ)
259244, 242mulcld 10650 . . . . . . . 8 (𝑋 ∈ ℂ → ((1 / 2) · 𝑋) ∈ ℂ)
260258, 259addcld 10649 . . . . . . 7 (𝑋 ∈ ℂ → (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋)) ∈ ℂ)
261191, 260mulcld 10650 . . . . . 6 (𝑋 ∈ ℂ → (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))) ∈ ℂ)
262254, 261addcomd 10831 . . . . 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 10654 . . . . . . 7 (𝑋 ∈ ℂ → (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))) = ((2 · ((𝑋↑3) − ((3 / 2) · (𝑋↑2)))) + (2 · ((1 / 2) · 𝑋))))
264191, 222, 257subdid 11085 . . . . . . . 8 (𝑋 ∈ ℂ → (2 · ((𝑋↑3) − ((3 / 2) · (𝑋↑2)))) = ((2 · (𝑋↑3)) − (2 · ((3 / 2) · (𝑋↑2)))))
26587, 204recidi 11360 . . . . . . . . . 10 (2 · (1 / 2)) = 1
266265oveq1i 7155 . . . . . . . . 9 ((2 · (1 / 2)) · 𝑋) = (1 · 𝑋)
267191, 244, 242mulassd 10653 . . . . . . . . 9 (𝑋 ∈ ℂ → ((2 · (1 / 2)) · 𝑋) = (2 · ((1 / 2) · 𝑋)))
268 mulid2 10629 . . . . . . . . 9 (𝑋 ∈ ℂ → (1 · 𝑋) = 𝑋)
269266, 267, 2683eqtr3a 2880 . . . . . . . 8 (𝑋 ∈ ℂ → (2 · ((1 / 2) · 𝑋)) = 𝑋)
270264, 269oveq12d 7163 . . . . . . 7 (𝑋 ∈ ℂ → ((2 · ((𝑋↑3) − ((3 / 2) · (𝑋↑2)))) + (2 · ((1 / 2) · 𝑋))) = (((2 · (𝑋↑3)) − (2 · ((3 / 2) · (𝑋↑2)))) + 𝑋))
271263, 270eqtrd 2856 . . . . . 6 (𝑋 ∈ ℂ → (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))) = (((2 · (𝑋↑3)) − (2 · ((3 / 2) · (𝑋↑2)))) + 𝑋))
272271oveq1d 7160 . . . . 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 10650 . . . . . . . 8 (𝑋 ∈ ℂ → (2 · ((3 / 2) · (𝑋↑2))) ∈ ℂ)
274223, 273subcld 10986 . . . . . . 7 (𝑋 ∈ ℂ → ((2 · (𝑋↑3)) − (2 · ((3 / 2) · (𝑋↑2)))) ∈ ℂ)
275274, 242, 254addassd 10652 . . . . . 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 10649 . . . . . . 7 (𝑋 ∈ ℂ → (𝑋 + (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))) ∈ ℂ)
277223, 273, 276subsubd 11014 . . . . . 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)))))))
27858, 87, 204divcan2i 11372 . . . . . . . . . . 11 (2 · (3 / 2)) = 3
279278oveq1i 7155 . . . . . . . . . 10 ((2 · (3 / 2)) · (𝑋↑2)) = (3 · (𝑋↑2))
280191, 256, 224mulassd 10653 . . . . . . . . . 10 (𝑋 ∈ ℂ → ((2 · (3 / 2)) · (𝑋↑2)) = (2 · ((3 / 2) · (𝑋↑2))))
281279, 280syl5reqr 2871 . . . . . . . . 9 (𝑋 ∈ ℂ → (2 · ((3 / 2) · (𝑋↑2))) = (3 · (𝑋↑2)))
282281oveq1d 7160 . . . . . . . 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 10855 . . . . . . . . . 10 (𝑋 ∈ ℂ → (𝑋 + (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))) = (((1 / 5) + (𝑋 − (1 / 2))) + (𝑋 + (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))))
284191, 247, 251adddid 10654 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → (2 · (((𝑋↑2) − 𝑋) + (1 / 6))) = ((2 · ((𝑋↑2) − 𝑋)) + (2 · (1 / 6))))
285191, 224, 242subdid 11085 . . . . . . . . . . . . . . 15 (𝑋 ∈ ℂ → (2 · ((𝑋↑2) − 𝑋)) = ((2 · (𝑋↑2)) − (2 · 𝑋)))
286187oveq2i 7156 . . . . . . . . . . . . . . . . 17 (2 / (3 · 2)) = (2 / 6)
28758, 184reccli 11359 . . . . . . . . . . . . . . . . . . . 20 (1 / 3) ∈ ℂ
28858, 87, 287mul32i 10825 . . . . . . . . . . . . . . . . . . 19 ((3 · 2) · (1 / 3)) = ((3 · (1 / 3)) · 2)
28958, 184recidi 11360 . . . . . . . . . . . . . . . . . . . . 21 (3 · (1 / 3)) = 1
290289oveq1i 7155 . . . . . . . . . . . . . . . . . . . 20 ((3 · (1 / 3)) · 2) = (1 · 2)
29187mulid2i 10635 . . . . . . . . . . . . . . . . . . . 20 (1 · 2) = 2
292290, 291eqtri 2844 . . . . . . . . . . . . . . . . . . 19 ((3 · (1 / 3)) · 2) = 2
293288, 292eqtri 2844 . . . . . . . . . . . . . . . . . 18 ((3 · 2) · (1 / 3)) = 2
294187, 178eqeltri 2909 . . . . . . . . . . . . . . . . . . 19 (3 · 2) ∈ ℂ
295187, 249eqnetri 3086 . . . . . . . . . . . . . . . . . . 19 (3 · 2) ≠ 0
29687, 294, 287, 295divmuli 11383 . . . . . . . . . . . . . . . . . 18 ((2 / (3 · 2)) = (1 / 3) ↔ ((3 · 2) · (1 / 3)) = 2)
297293, 296mpbir 232 . . . . . . . . . . . . . . . . 17 (2 / (3 · 2)) = (1 / 3)
29887, 178, 249divreci 11374 . . . . . . . . . . . . . . . . 17 (2 / 6) = (2 · (1 / 6))
299286, 297, 2983eqtr3ri 2853 . . . . . . . . . . . . . . . 16 (2 · (1 / 6)) = (1 / 3)
300299a1i 11 . . . . . . . . . . . . . . 15 (𝑋 ∈ ℂ → (2 · (1 / 6)) = (1 / 3))
301285, 300oveq12d 7163 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → ((2 · ((𝑋↑2) − 𝑋)) + (2 · (1 / 6))) = (((2 · (𝑋↑2)) − (2 · 𝑋)) + (1 / 3)))
302284, 301eqtrd 2856 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (2 · (((𝑋↑2) − 𝑋) + (1 / 6))) = (((2 · (𝑋↑2)) − (2 · 𝑋)) + (1 / 3)))
303302oveq2d 7161 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → (𝑋 + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))) = (𝑋 + (((2 · (𝑋↑2)) − (2 · 𝑋)) + (1 / 3))))
304191, 224mulcld 10650 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → (2 · (𝑋↑2)) ∈ ℂ)
305191, 242mulcld 10650 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → (2 · 𝑋) ∈ ℂ)
306304, 305subcld 10986 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → ((2 · (𝑋↑2)) − (2 · 𝑋)) ∈ ℂ)
307287a1i 11 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (1 / 3) ∈ ℂ)
308242, 306, 307addassd 10652 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → ((𝑋 + ((2 · (𝑋↑2)) − (2 · 𝑋))) + (1 / 3)) = (𝑋 + (((2 · (𝑋↑2)) − (2 · 𝑋)) + (1 / 3))))
309242, 304, 305addsub12d 11009 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (𝑋 + ((2 · (𝑋↑2)) − (2 · 𝑋))) = ((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))))
310309oveq1d 7160 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → ((𝑋 + ((2 · (𝑋↑2)) − (2 · 𝑋))) + (1 / 3)) = (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3)))
311303, 308, 3103eqtr2d 2862 . . . . . . . . . . 11 (𝑋 ∈ ℂ → (𝑋 + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))) = (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3)))
312311oveq2d 7161 . . . . . . . . . 10 (𝑋 ∈ ℂ → (((1 / 5) + (𝑋 − (1 / 2))) + (𝑋 + (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))) = (((1 / 5) + (𝑋 − (1 / 2))) + (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3))))
313283, 312eqtrd 2856 . . . . . . . . 9 (𝑋 ∈ ℂ → (𝑋 + (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))) = (((1 / 5) + (𝑋 − (1 / 2))) + (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3))))
314313oveq2d 7161 . . . . . . . 8 (𝑋 ∈ ℂ → ((3 · (𝑋↑2)) − (𝑋 + (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))))) = ((3 · (𝑋↑2)) − (((1 / 5) + (𝑋 − (1 / 2))) + (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3)))))
315242, 305subcld 10986 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (𝑋 − (2 · 𝑋)) ∈ ℂ)
316304, 315addcld 10649 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → ((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) ∈ ℂ)
317241, 245, 316, 307add4d 10857 . . . . . . . . . . 11 (𝑋 ∈ ℂ → (((1 / 5) + (𝑋 − (1 / 2))) + (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3))) = (((1 / 5) + ((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋)))) + ((𝑋 − (1 / 2)) + (1 / 3))))
318241, 304, 315add12d 10855 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → ((1 / 5) + ((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋)))) = ((2 · (𝑋↑2)) + ((1 / 5) + (𝑋 − (2 · 𝑋)))))
319318oveq1d 7160 . . . . . . . . . . 11 (𝑋 ∈ ℂ → (((1 / 5) + ((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋)))) + ((𝑋 − (1 / 2)) + (1 / 3))) = (((2 · (𝑋↑2)) + ((1 / 5) + (𝑋 − (2 · 𝑋)))) + ((𝑋 − (1 / 2)) + (1 / 3))))
320241, 315addcld 10649 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → ((1 / 5) + (𝑋 − (2 · 𝑋))) ∈ ℂ)
321245, 307addcld 10649 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → ((𝑋 − (1 / 2)) + (1 / 3)) ∈ ℂ)
322304, 320, 321addassd 10652 . . . . . . . . . . 11 (𝑋 ∈ ℂ → (((2 · (𝑋↑2)) + ((1 / 5) + (𝑋 − (2 · 𝑋)))) + ((𝑋 − (1 / 2)) + (1 / 3))) = ((2 · (𝑋↑2)) + (((1 / 5) + (𝑋 − (2 · 𝑋))) + ((𝑋 − (1 / 2)) + (1 / 3)))))
323317, 319, 3223eqtrd 2860 . . . . . . . . . 10 (𝑋 ∈ ℂ → (((1 / 5) + (𝑋 − (1 / 2))) + (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3))) = ((2 · (𝑋↑2)) + (((1 / 5) + (𝑋 − (2 · 𝑋))) + ((𝑋 − (1 / 2)) + (1 / 3)))))
324323oveq2d 7161 . . . . . . . . 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 10650 . . . . . . . . . 10 (𝑋 ∈ ℂ → (3 · (𝑋↑2)) ∈ ℂ)
326320, 321addcld 10649 . . . . . . . . . 10 (𝑋 ∈ ℂ → (((1 / 5) + (𝑋 − (2 · 𝑋))) + ((𝑋 − (1 / 2)) + (1 / 3))) ∈ ℂ)
327325, 304, 326subsub4d 11017 . . . . . . . . 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 10964 . . . . . . . . . . . 12 (3 − 2) = 1
329328oveq1i 7155 . . . . . . . . . . 11 ((3 − 2) · (𝑋↑2)) = (1 · (𝑋↑2))
330183, 191, 224subdird 11086 . . . . . . . . . . 11 (𝑋 ∈ ℂ → ((3 − 2) · (𝑋↑2)) = ((3 · (𝑋↑2)) − (2 · (𝑋↑2))))
331224mulid2d 10648 . . . . . . . . . . 11 (𝑋 ∈ ℂ → (1 · (𝑋↑2)) = (𝑋↑2))
332329, 330, 3313eqtr3a 2880 . . . . . . . . . 10 (𝑋 ∈ ℂ → ((3 · (𝑋↑2)) − (2 · (𝑋↑2))) = (𝑋↑2))
333241, 305, 242subsubd 11014 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → ((1 / 5) − ((2 · 𝑋) − 𝑋)) = (((1 / 5) − (2 · 𝑋)) + 𝑋))
334 2txmxeqx 11766 . . . . . . . . . . . . . 14 (𝑋 ∈ ℂ → ((2 · 𝑋) − 𝑋) = 𝑋)
335334oveq2d 7161 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → ((1 / 5) − ((2 · 𝑋) − 𝑋)) = ((1 / 5) − 𝑋))
336241, 305, 242subadd23d 11008 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (((1 / 5) − (2 · 𝑋)) + 𝑋) = ((1 / 5) + (𝑋 − (2 · 𝑋))))
337333, 335, 3363eqtr3d 2864 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → ((1 / 5) − 𝑋) = ((1 / 5) + (𝑋 − (2 · 𝑋))))
338242, 244, 307subsubd 11014 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → (𝑋 − ((1 / 2) − (1 / 3))) = ((𝑋 − (1 / 2)) + (1 / 3)))
339337, 338oveq12d 7163 . . . . . . . . . . 11 (𝑋 ∈ ℂ → (((1 / 5) − 𝑋) + (𝑋 − ((1 / 2) − (1 / 3)))) = (((1 / 5) + (𝑋 − (2 · 𝑋))) + ((𝑋 − (1 / 2)) + (1 / 3))))
340243, 287subcli 10951 . . . . . . . . . . . . . 14 ((1 / 2) − (1 / 3)) ∈ ℂ
341340a1i 11 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → ((1 / 2) − (1 / 3)) ∈ ℂ)
342241, 242, 341npncand 11010 . . . . . . . . . . . 12 (𝑋 ∈ ℂ → (((1 / 5) − 𝑋) + (𝑋 − ((1 / 2) − (1 / 3)))) = ((1 / 5) − ((1 / 2) − (1 / 3))))
343 halfthird 12230 . . . . . . . . . . . . . 14 ((1 / 2) − (1 / 3)) = (1 / 6)
344343oveq2i 7156 . . . . . . . . . . . . 13 ((1 / 5) − ((1 / 2) − (1 / 3))) = ((1 / 5) − (1 / 6))
345 5recm6rec 12231 . . . . . . . . . . . . 13 ((1 / 5) − (1 / 6)) = (1 / 30)
346344, 345eqtri 2844 . . . . . . . . . . . 12 ((1 / 5) − ((1 / 2) − (1 / 3))) = (1 / 30)
347342, 346syl6eq 2872 . . . . . . . . . . 11 (𝑋 ∈ ℂ → (((1 / 5) − 𝑋) + (𝑋 − ((1 / 2) − (1 / 3)))) = (1 / 30))
348339, 347eqtr3d 2858 . . . . . . . . . 10 (𝑋 ∈ ℂ → (((1 / 5) + (𝑋 − (2 · 𝑋))) + ((𝑋 − (1 / 2)) + (1 / 3))) = (1 / 30))
349332, 348oveq12d 7163 . . . . . . . . 9 (𝑋 ∈ ℂ → (((3 · (𝑋↑2)) − (2 · (𝑋↑2))) − (((1 / 5) + (𝑋 − (2 · 𝑋))) + ((𝑋 − (1 / 2)) + (1 / 3)))) = ((𝑋↑2) − (1 / 30)))
350324, 327, 3493eqtr2d 2862 . . . . . . . 8 (𝑋 ∈ ℂ → ((3 · (𝑋↑2)) − (((1 / 5) + (𝑋 − (1 / 2))) + (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3)))) = ((𝑋↑2) − (1 / 30)))
351282, 314, 3503eqtrd 2860 . . . . . . 7 (𝑋 ∈ ℂ → ((2 · ((3 / 2) · (𝑋↑2))) − (𝑋 + (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))))) = ((𝑋↑2) − (1 / 30)))
352351oveq2d 7161 . . . . . 6 (𝑋 ∈ ℂ → ((2 · (𝑋↑3)) − ((2 · ((3 / 2) · (𝑋↑2))) − (𝑋 + (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))))) = ((2 · (𝑋↑3)) − ((𝑋↑2) − (1 / 30))))
353275, 277, 3523eqtr2d 2862 . . . . 5 (𝑋 ∈ ℂ → ((((2 · (𝑋↑3)) − (2 · ((3 / 2) · (𝑋↑2)))) + 𝑋) + (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))) = ((2 · (𝑋↑3)) − ((𝑋↑2) − (1 / 30))))
354262, 272, 3533eqtrd 2860 . . . 4 (𝑋 ∈ ℂ → ((((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))) + (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋)))) = ((2 · (𝑋↑3)) − ((𝑋↑2) − (1 / 30))))
355354oveq2d 7161 . . 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 10986 . . . 4 (𝑋 ∈ ℂ → ((𝑋↑4) − (2 · (𝑋↑3))) ∈ ℂ)
357356, 224, 238addsubassd 11006 . . 3 (𝑋 ∈ ℂ → ((((𝑋↑4) − (2 · (𝑋↑3))) + (𝑋↑2)) − (1 / 30)) = (((𝑋↑4) − (2 · (𝑋↑3))) + ((𝑋↑2) − (1 / 30))))
358240, 355, 3573eqtr4d 2866 . 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 2860 1 (𝑋 ∈ ℂ → (4 BernPoly 𝑋) = ((((𝑋↑4) − (2 · (𝑋↑3))) + (𝑋↑2)) − (1 / 30)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1528  wcel 2105  wne 3016  wss 3935   class class class wbr 5058  cfv 6349  (class class class)co 7145  cc 10524  cr 10525  0cc0 10526  1c1 10527   + caddc 10529   · cmul 10531   < clt 10664  cmin 10859   / cdiv 11286  cn 11627  2c2 11681  3c3 11682  4c4 11683  5c5 11684  6c6 11685  0cn0 11886  cz 11970  cdc 12087  cuz 12232  ...cfz 12882  cexp 13419  Ccbc 13652  Σcsu 15032   BernPoly cbp 15390
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-inf2 9093  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-fal 1541  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4833  df-int 4870  df-iun 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-se 5509  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-isom 6358  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7569  df-1st 7680  df-2nd 7681  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-1o 8093  df-oadd 8097  df-er 8279  df-en 8499  df-dom 8500  df-sdom 8501  df-fin 8502  df-sup 8895  df-oi 8963  df-card 9357  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11628  df-2 11689  df-3 11690  df-4 11691  df-5 11692  df-6 11693  df-7 11694  df-8 11695  df-9 11696  df-n0 11887  df-z 11971  df-dec 12088  df-uz 12233  df-rp 12380  df-fz 12883  df-fzo 13024  df-seq 13360  df-exp 13420  df-fac 13624  df-bc 13653  df-hash 13681  df-cj 14448  df-re 14449  df-im 14450  df-sqrt 14584  df-abs 14585  df-clim 14835  df-sum 15033  df-bpoly 15391
This theorem is referenced by:  fsumcube  15404
  Copyright terms: Public domain W3C validator