| Step | Hyp | Ref
| Expression |
| 1 | | 4nn0 12545 |
. . 3
⊢ 4 ∈
ℕ0 |
| 2 | | bpolyval 16085 |
. . 3
⊢ ((4
∈ ℕ0 ∧ 𝑋 ∈ ℂ) → (4 BernPoly 𝑋) = ((𝑋↑4) − Σ𝑘 ∈ (0...(4 − 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))))) |
| 3 | 1, 2 | mpan 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) |
| 6 | 4, 5 | eqtri 2765 |
. . . . . 6
⊢ (4
− 1) = (2 + 1) |
| 7 | 6 | oveq2i 7442 |
. . . . 5
⊢ (0...(4
− 1)) = (0...(2 + 1)) |
| 8 | 7 | sumeq1i 15733 |
. . . 4
⊢
Σ𝑘 ∈
(0...(4 − 1))((4C𝑘)
· ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = Σ𝑘 ∈ (0...(2 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) |
| 9 | | 2eluzge0 12935 |
. . . . . . 7
⊢ 2 ∈
(ℤ≥‘0) |
| 10 | 9 | a1i 11 |
. . . . . 6
⊢ (𝑋 ∈ ℂ → 2 ∈
(ℤ≥‘0)) |
| 11 | | elfzelz 13564 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...(2 + 1)) →
𝑘 ∈
ℤ) |
| 12 | | bccl 14361 |
. . . . . . . . . 10
⊢ ((4
∈ ℕ0 ∧ 𝑘 ∈ ℤ) → (4C𝑘) ∈
ℕ0) |
| 13 | 1, 11, 12 | sylancr 587 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...(2 + 1)) →
(4C𝑘) ∈
ℕ0) |
| 14 | 13 | nn0cnd 12589 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...(2 + 1)) →
(4C𝑘) ∈
ℂ) |
| 15 | 14 | adantl 481 |
. . . . . . 7
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(2 + 1))) →
(4C𝑘) ∈
ℂ) |
| 16 | | elfznn0 13660 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...(2 + 1)) →
𝑘 ∈
ℕ0) |
| 17 | | bpolycl 16088 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (𝑘 BernPoly 𝑋) ∈
ℂ) |
| 18 | 16, 17 | sylan 580 |
. . . . . . . . 9
⊢ ((𝑘 ∈ (0...(2 + 1)) ∧
𝑋 ∈ ℂ) →
(𝑘 BernPoly 𝑋) ∈
ℂ) |
| 19 | 18 | ancoms 458 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(2 + 1))) →
(𝑘 BernPoly 𝑋) ∈
ℂ) |
| 20 | | 4re 12350 |
. . . . . . . . . . . . 13
⊢ 4 ∈
ℝ |
| 21 | 20 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (0...(2 + 1)) → 4
∈ ℝ) |
| 22 | 11 | zred 12722 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (0...(2 + 1)) →
𝑘 ∈
ℝ) |
| 23 | 21, 22 | resubcld 11691 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (0...(2 + 1)) → (4
− 𝑘) ∈
ℝ) |
| 24 | | peano2re 11434 |
. . . . . . . . . . 11
⊢ ((4
− 𝑘) ∈ ℝ
→ ((4 − 𝑘) + 1)
∈ ℝ) |
| 25 | 23, 24 | syl 17 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...(2 + 1)) → ((4
− 𝑘) + 1) ∈
ℝ) |
| 26 | 25 | recnd 11289 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...(2 + 1)) → ((4
− 𝑘) + 1) ∈
ℂ) |
| 27 | 26 | adantl 481 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(2 + 1))) →
((4 − 𝑘) + 1) ∈
ℂ) |
| 28 | | 1red 11262 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (0...(2 + 1)) → 1
∈ ℝ) |
| 29 | 5 | oveq2i 7442 |
. . . . . . . . . . . . . 14
⊢ (0...3) =
(0...(2 + 1)) |
| 30 | 29 | eleq2i 2833 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0...3) ↔ 𝑘 ∈ (0...(2 +
1))) |
| 31 | | elfzelz 13564 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (0...3) → 𝑘 ∈
ℤ) |
| 32 | 31 | zred 12722 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (0...3) → 𝑘 ∈
ℝ) |
| 33 | | 3re 12346 |
. . . . . . . . . . . . . . 15
⊢ 3 ∈
ℝ |
| 34 | 33 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (0...3) → 3 ∈
ℝ) |
| 35 | 20 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (0...3) → 4 ∈
ℝ) |
| 36 | | elfzle2 13568 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (0...3) → 𝑘 ≤ 3) |
| 37 | | 3lt4 12440 |
. . . . . . . . . . . . . . 15
⊢ 3 <
4 |
| 38 | 37 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (0...3) → 3 <
4) |
| 39 | 32, 34, 35, 36, 38 | lelttrd 11419 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0...3) → 𝑘 < 4) |
| 40 | 30, 39 | sylbir 235 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (0...(2 + 1)) →
𝑘 < 4) |
| 41 | 22, 21 | posdifd 11850 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (0...(2 + 1)) →
(𝑘 < 4 ↔ 0 < (4
− 𝑘))) |
| 42 | 40, 41 | mpbid 232 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (0...(2 + 1)) → 0
< (4 − 𝑘)) |
| 43 | | 0lt1 11785 |
. . . . . . . . . . . 12
⊢ 0 <
1 |
| 44 | 43 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (0...(2 + 1)) → 0
< 1) |
| 45 | 23, 28, 42, 44 | addgt0d 11838 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...(2 + 1)) → 0
< ((4 − 𝑘) +
1)) |
| 46 | 45 | gt0ne0d 11827 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...(2 + 1)) → ((4
− 𝑘) + 1) ≠
0) |
| 47 | 46 | adantl 481 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(2 + 1))) →
((4 − 𝑘) + 1) ≠
0) |
| 48 | 19, 27, 47 | divcld 12043 |
. . . . . . 7
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(2 + 1))) →
((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)) ∈
ℂ) |
| 49 | 15, 48 | mulcld 11281 |
. . . . . 6
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(2 + 1))) →
((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) ∈ ℂ) |
| 50 | 5 | eqeq2i 2750 |
. . . . . . 7
⊢ (𝑘 = 3 ↔ 𝑘 = (2 + 1)) |
| 51 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑘 = 3 → (4C𝑘) = (4C3)) |
| 52 | | 4bc3eq4 14367 |
. . . . . . . . 9
⊢ (4C3) =
4 |
| 53 | 51, 52 | eqtrdi 2793 |
. . . . . . . 8
⊢ (𝑘 = 3 → (4C𝑘) = 4) |
| 54 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑘 = 3 → (𝑘 BernPoly 𝑋) = (3 BernPoly 𝑋)) |
| 55 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑘 = 3 → (4 − 𝑘) = (4 −
3)) |
| 56 | 55 | oveq1d 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 |
| 61 | 57, 58, 59, 60 | subaddrii 11598 |
. . . . . . . . . . . 12
⊢ (4
− 3) = 1 |
| 62 | 61 | oveq1i 7441 |
. . . . . . . . . . 11
⊢ ((4
− 3) + 1) = (1 + 1) |
| 63 | | df-2 12329 |
. . . . . . . . . . 11
⊢ 2 = (1 +
1) |
| 64 | 62, 63 | eqtr4i 2768 |
. . . . . . . . . 10
⊢ ((4
− 3) + 1) = 2 |
| 65 | 56, 64 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (𝑘 = 3 → ((4 − 𝑘) + 1) = 2) |
| 66 | 54, 65 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝑘 = 3 → ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)) = ((3 BernPoly 𝑋) / 2)) |
| 67 | 53, 66 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑘 = 3 → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (4 · ((3 BernPoly 𝑋) / 2))) |
| 68 | 50, 67 | sylbir 235 |
. . . . . 6
⊢ (𝑘 = (2 + 1) → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (4 · ((3 BernPoly 𝑋) / 2))) |
| 69 | 10, 49, 68 | fsump1 15792 |
. . . . 5
⊢ (𝑋 ∈ ℂ →
Σ𝑘 ∈ (0...(2 +
1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (Σ𝑘 ∈ (0...2)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) + (4 · ((3 BernPoly 𝑋) / 2)))) |
| 70 | 63 | oveq2i 7442 |
. . . . . . . 8
⊢ (0...2) =
(0...(1 + 1)) |
| 71 | 70 | sumeq1i 15733 |
. . . . . . 7
⊢
Σ𝑘 ∈
(0...2)((4C𝑘) ·
((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = Σ𝑘 ∈ (0...(1 + 1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) |
| 72 | | 1eluzge0 12934 |
. . . . . . . . . 10
⊢ 1 ∈
(ℤ≥‘0) |
| 73 | 72 | a1i 11 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℂ → 1 ∈
(ℤ≥‘0)) |
| 74 | | fzssp1 13607 |
. . . . . . . . . . . 12
⊢ (0...(1 +
1)) ⊆ (0...((1 + 1) + 1)) |
| 75 | 63 | oveq1i 7441 |
. . . . . . . . . . . . 13
⊢ (2 + 1) =
((1 + 1) + 1) |
| 76 | 75 | oveq2i 7442 |
. . . . . . . . . . . 12
⊢ (0...(2 +
1)) = (0...((1 + 1) + 1)) |
| 77 | 74, 76 | sseqtrri 4033 |
. . . . . . . . . . 11
⊢ (0...(1 +
1)) ⊆ (0...(2 + 1)) |
| 78 | 77 | sseli 3979 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...(1 + 1)) →
𝑘 ∈ (0...(2 +
1))) |
| 79 | 78, 49 | sylan2 593 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(1 + 1))) →
((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) ∈ ℂ) |
| 80 | 63 | eqeq2i 2750 |
. . . . . . . . . 10
⊢ (𝑘 = 2 ↔ 𝑘 = (1 + 1)) |
| 81 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑘 = 2 → (4C𝑘) = (4C2)) |
| 82 | | 4bc2eq6 14368 |
. . . . . . . . . . . 12
⊢ (4C2) =
6 |
| 83 | 81, 82 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (𝑘 = 2 → (4C𝑘) = 6) |
| 84 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑘 = 2 → (𝑘 BernPoly 𝑋) = (2 BernPoly 𝑋)) |
| 85 | | oveq2 7439 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 2 → (4 − 𝑘) = (4 −
2)) |
| 86 | 85 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 2 → ((4 − 𝑘) + 1) = ((4 − 2) +
1)) |
| 87 | | 2cn 12341 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℂ |
| 88 | | 2p2e4 12401 |
. . . . . . . . . . . . . . . 16
⊢ (2 + 2) =
4 |
| 89 | 57, 87, 87, 88 | subaddrii 11598 |
. . . . . . . . . . . . . . 15
⊢ (4
− 2) = 2 |
| 90 | 89 | oveq1i 7441 |
. . . . . . . . . . . . . 14
⊢ ((4
− 2) + 1) = (2 + 1) |
| 91 | 90, 5 | eqtr4i 2768 |
. . . . . . . . . . . . 13
⊢ ((4
− 2) + 1) = 3 |
| 92 | 86, 91 | eqtrdi 2793 |
. . . . . . . . . . . 12
⊢ (𝑘 = 2 → ((4 − 𝑘) + 1) = 3) |
| 93 | 84, 92 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (𝑘 = 2 → ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)) = ((2 BernPoly 𝑋) / 3)) |
| 94 | 83, 93 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝑘 = 2 → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (6 · ((2 BernPoly 𝑋) / 3))) |
| 95 | 80, 94 | sylbir 235 |
. . . . . . . . 9
⊢ (𝑘 = (1 + 1) → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (6 · ((2 BernPoly 𝑋) / 3))) |
| 96 | 73, 79, 95 | fsump1 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 |
| 98 | 97 | oveq2i 7442 |
. . . . . . . . . . 11
⊢ (0...(0 +
1)) = (0...1) |
| 99 | 98 | sumeq1i 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) |
| 102 | 100, 101 | eleqtri 2839 |
. . . . . . . . . . . . 13
⊢ 0 ∈
(ℤ≥‘0) |
| 103 | 102 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → 0 ∈
(ℤ≥‘0)) |
| 104 | | 3nn 12345 |
. . . . . . . . . . . . . . . . 17
⊢ 3 ∈
ℕ |
| 105 | | nnuz 12921 |
. . . . . . . . . . . . . . . . 17
⊢ ℕ =
(ℤ≥‘1) |
| 106 | 104, 105 | eleqtri 2839 |
. . . . . . . . . . . . . . . 16
⊢ 3 ∈
(ℤ≥‘1) |
| 107 | | fzss2 13604 |
. . . . . . . . . . . . . . . 16
⊢ (3 ∈
(ℤ≥‘1) → (0...1) ⊆
(0...3)) |
| 108 | 106, 107 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (0...1)
⊆ (0...3) |
| 109 | | 2p1e3 12408 |
. . . . . . . . . . . . . . . 16
⊢ (2 + 1) =
3 |
| 110 | 109 | oveq2i 7442 |
. . . . . . . . . . . . . . 15
⊢ (0...(2 +
1)) = (0...3) |
| 111 | 108, 98, 110 | 3sstr4i 4035 |
. . . . . . . . . . . . . 14
⊢ (0...(0 +
1)) ⊆ (0...(2 + 1)) |
| 112 | 111 | sseli 3979 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0...(0 + 1)) →
𝑘 ∈ (0...(2 +
1))) |
| 113 | 112, 49 | sylan2 593 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(0 + 1))) →
((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) ∈ ℂ) |
| 114 | 97 | eqeq2i 2750 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (0 + 1) ↔ 𝑘 = 1) |
| 115 | | oveq2 7439 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 1 → (4C𝑘) = (4C1)) |
| 116 | | bcn1 14352 |
. . . . . . . . . . . . . . . 16
⊢ (4 ∈
ℕ0 → (4C1) = 4) |
| 117 | 1, 116 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (4C1) =
4 |
| 118 | 115, 117 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 1 → (4C𝑘) = 4) |
| 119 | | oveq1 7438 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 1 → (𝑘 BernPoly 𝑋) = (1 BernPoly 𝑋)) |
| 120 | | oveq2 7439 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 1 → (4 − 𝑘) = (4 −
1)) |
| 121 | 120 | oveq1d 7446 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 1 → ((4 − 𝑘) + 1) = ((4 − 1) +
1)) |
| 122 | 4 | oveq1i 7441 |
. . . . . . . . . . . . . . . . 17
⊢ ((4
− 1) + 1) = (3 + 1) |
| 123 | | df-4 12331 |
. . . . . . . . . . . . . . . . 17
⊢ 4 = (3 +
1) |
| 124 | 122, 123 | eqtr4i 2768 |
. . . . . . . . . . . . . . . 16
⊢ ((4
− 1) + 1) = 4 |
| 125 | 121, 124 | eqtrdi 2793 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 1 → ((4 − 𝑘) + 1) = 4) |
| 126 | 119, 125 | oveq12d 7449 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 1 → ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)) = ((1 BernPoly 𝑋) / 4)) |
| 127 | 118, 126 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 1 → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (4 · ((1 BernPoly 𝑋) / 4))) |
| 128 | 114, 127 | sylbi 217 |
. . . . . . . . . . . 12
⊢ (𝑘 = (0 + 1) → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (4 · ((1 BernPoly 𝑋) / 4))) |
| 129 | 103, 113,
128 | fsump1 15792 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ →
Σ𝑘 ∈ (0...(0 +
1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (Σ𝑘 ∈ (0...0)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) + (4 · ((1 BernPoly 𝑋) / 4)))) |
| 130 | | 0z 12624 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℤ |
| 131 | 59 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 ∈ ℂ → 1 ∈
ℂ) |
| 132 | | bpolycl 16088 |
. . . . . . . . . . . . . . . . 17
⊢ ((0
∈ ℕ0 ∧ 𝑋 ∈ ℂ) → (0 BernPoly 𝑋) ∈
ℂ) |
| 133 | 100, 132 | mpan 690 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 ∈ ℂ → (0
BernPoly 𝑋) ∈
ℂ) |
| 134 | | 5cn 12354 |
. . . . . . . . . . . . . . . . 17
⊢ 5 ∈
ℂ |
| 135 | 134 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 ∈ ℂ → 5 ∈
ℂ) |
| 136 | | 0re 11263 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
ℝ |
| 137 | | 5pos 12375 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 <
5 |
| 138 | 136, 137 | gtneii 11373 |
. . . . . . . . . . . . . . . . 17
⊢ 5 ≠
0 |
| 139 | 138 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 ∈ ℂ → 5 ≠
0) |
| 140 | 133, 135,
139 | divcld 12043 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 ∈ ℂ → ((0
BernPoly 𝑋) / 5) ∈
ℂ) |
| 141 | 131, 140 | mulcld 11281 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ ℂ → (1
· ((0 BernPoly 𝑋) /
5)) ∈ ℂ) |
| 142 | | oveq2 7439 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 0 → (4C𝑘) = (4C0)) |
| 143 | | bcn0 14349 |
. . . . . . . . . . . . . . . . . 18
⊢ (4 ∈
ℕ0 → (4C0) = 1) |
| 144 | 1, 143 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (4C0) =
1 |
| 145 | 142, 144 | eqtrdi 2793 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 0 → (4C𝑘) = 1) |
| 146 | | oveq1 7438 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 0 → (𝑘 BernPoly 𝑋) = (0 BernPoly 𝑋)) |
| 147 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 0 → (4 − 𝑘) = (4 −
0)) |
| 148 | 147 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 0 → ((4 − 𝑘) + 1) = ((4 − 0) +
1)) |
| 149 | 57 | subid1i 11581 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (4
− 0) = 4 |
| 150 | 149 | oveq1i 7441 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((4
− 0) + 1) = (4 + 1) |
| 151 | | 4p1e5 12412 |
. . . . . . . . . . . . . . . . . . 19
⊢ (4 + 1) =
5 |
| 152 | 150, 151 | eqtri 2765 |
. . . . . . . . . . . . . . . . . 18
⊢ ((4
− 0) + 1) = 5 |
| 153 | 148, 152 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 0 → ((4 − 𝑘) + 1) = 5) |
| 154 | 146, 153 | oveq12d 7449 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 0 → ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1)) = ((0 BernPoly 𝑋) / 5)) |
| 155 | 145, 154 | oveq12d 7449 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 0 → ((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (1 · ((0 BernPoly 𝑋) / 5))) |
| 156 | 155 | fsum1 15783 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℤ ∧ (1 · ((0 BernPoly 𝑋) / 5)) ∈ ℂ) → Σ𝑘 ∈ (0...0)((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (1 · ((0 BernPoly 𝑋) / 5))) |
| 157 | 130, 141,
156 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ →
Σ𝑘 ∈
(0...0)((4C𝑘) ·
((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (1 · ((0
BernPoly 𝑋) /
5))) |
| 158 | | bpoly0 16086 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 ∈ ℂ → (0
BernPoly 𝑋) =
1) |
| 159 | 158 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 ∈ ℂ → ((0
BernPoly 𝑋) / 5) = (1 /
5)) |
| 160 | 159 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ ℂ → (1
· ((0 BernPoly 𝑋) /
5)) = (1 · (1 / 5))) |
| 161 | 134, 138 | reccli 11997 |
. . . . . . . . . . . . . . 15
⊢ (1 / 5)
∈ ℂ |
| 162 | 161 | mullidi 11266 |
. . . . . . . . . . . . . 14
⊢ (1
· (1 / 5)) = (1 / 5) |
| 163 | 160, 162 | eqtrdi 2793 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → (1
· ((0 BernPoly 𝑋) /
5)) = (1 / 5)) |
| 164 | 157, 163 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ →
Σ𝑘 ∈
(0...0)((4C𝑘) ·
((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (1 /
5)) |
| 165 | | 1nn0 12542 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℕ0 |
| 166 | | bpolycl 16088 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℕ0 ∧ 𝑋 ∈ ℂ) → (1 BernPoly 𝑋) ∈
ℂ) |
| 167 | 165, 166 | mpan 690 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ ℂ → (1
BernPoly 𝑋) ∈
ℂ) |
| 168 | | nn0cn 12536 |
. . . . . . . . . . . . . . 15
⊢ (4 ∈
ℕ0 → 4 ∈ ℂ) |
| 169 | 1, 168 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ ℂ → 4 ∈
ℂ) |
| 170 | | 4ne0 12374 |
. . . . . . . . . . . . . . 15
⊢ 4 ≠
0 |
| 171 | 170 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ ℂ → 4 ≠
0) |
| 172 | 167, 169,
171 | divcan2d 12045 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → (4
· ((1 BernPoly 𝑋) /
4)) = (1 BernPoly 𝑋)) |
| 173 | | bpoly1 16087 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → (1
BernPoly 𝑋) = (𝑋 − (1 /
2))) |
| 174 | 172, 173 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → (4
· ((1 BernPoly 𝑋) /
4)) = (𝑋 − (1 /
2))) |
| 175 | 164, 174 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ →
(Σ𝑘 ∈
(0...0)((4C𝑘) ·
((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) + (4 · ((1
BernPoly 𝑋) / 4))) = ((1 /
5) + (𝑋 − (1 /
2)))) |
| 176 | 129, 175 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ →
Σ𝑘 ∈ (0...(0 +
1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = ((1 / 5) + (𝑋 − (1 / 2)))) |
| 177 | 99, 176 | eqtr3id 2791 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℂ →
Σ𝑘 ∈
(0...1)((4C𝑘) ·
((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = ((1 / 5) + (𝑋 − (1 /
2)))) |
| 178 | | 6cn 12357 |
. . . . . . . . . . . 12
⊢ 6 ∈
ℂ |
| 179 | 178 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → 6 ∈
ℂ) |
| 180 | | 2nn0 12543 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℕ0 |
| 181 | | bpolycl 16088 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℕ0 ∧ 𝑋 ∈ ℂ) → (2 BernPoly 𝑋) ∈
ℂ) |
| 182 | 180, 181 | mpan 690 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → (2
BernPoly 𝑋) ∈
ℂ) |
| 183 | 58 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → 3 ∈
ℂ) |
| 184 | | 3ne0 12372 |
. . . . . . . . . . . 12
⊢ 3 ≠
0 |
| 185 | 184 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → 3 ≠
0) |
| 186 | 179, 182,
183, 185 | div12d 12079 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ → (6
· ((2 BernPoly 𝑋) /
3)) = ((2 BernPoly 𝑋)
· (6 / 3))) |
| 187 | | 3t2e6 12432 |
. . . . . . . . . . . . 13
⊢ (3
· 2) = 6 |
| 188 | 178, 58, 87, 184 | divmuli 12021 |
. . . . . . . . . . . . 13
⊢ ((6 / 3)
= 2 ↔ (3 · 2) = 6) |
| 189 | 187, 188 | mpbir 231 |
. . . . . . . . . . . 12
⊢ (6 / 3) =
2 |
| 190 | 189 | oveq2i 7442 |
. . . . . . . . . . 11
⊢ ((2
BernPoly 𝑋) · (6 /
3)) = ((2 BernPoly 𝑋)
· 2) |
| 191 | 87 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → 2 ∈
ℂ) |
| 192 | 182, 191 | mulcomd 11282 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → ((2
BernPoly 𝑋) · 2) =
(2 · (2 BernPoly 𝑋))) |
| 193 | | bpoly2 16093 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → (2
BernPoly 𝑋) = (((𝑋↑2) − 𝑋) + (1 / 6))) |
| 194 | 193 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → (2
· (2 BernPoly 𝑋)) =
(2 · (((𝑋↑2)
− 𝑋) + (1 /
6)))) |
| 195 | 192, 194 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → ((2
BernPoly 𝑋) · 2) =
(2 · (((𝑋↑2)
− 𝑋) + (1 /
6)))) |
| 196 | 190, 195 | eqtrid 2789 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ → ((2
BernPoly 𝑋) · (6 /
3)) = (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))) |
| 197 | 186, 196 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℂ → (6
· ((2 BernPoly 𝑋) /
3)) = (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))) |
| 198 | 177, 197 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝑋 ∈ ℂ →
(Σ𝑘 ∈
(0...1)((4C𝑘) ·
((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) + (6 · ((2
BernPoly 𝑋) / 3))) = (((1 /
5) + (𝑋 − (1 / 2))) +
(2 · (((𝑋↑2)
− 𝑋) + (1 /
6))))) |
| 199 | 96, 198 | eqtrd 2777 |
. . . . . . 7
⊢ (𝑋 ∈ ℂ →
Σ𝑘 ∈ (0...(1 +
1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))) |
| 200 | 71, 199 | eqtrid 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 𝑋) ∈
ℂ) |
| 203 | 201, 202 | mpan 690 |
. . . . . . . 8
⊢ (𝑋 ∈ ℂ → (3
BernPoly 𝑋) ∈
ℂ) |
| 204 | | 2ne0 12370 |
. . . . . . . . 9
⊢ 2 ≠
0 |
| 205 | 204 | a1i 11 |
. . . . . . . 8
⊢ (𝑋 ∈ ℂ → 2 ≠
0) |
| 206 | 169, 203,
191, 205 | div12d 12079 |
. . . . . . 7
⊢ (𝑋 ∈ ℂ → (4
· ((3 BernPoly 𝑋) /
2)) = ((3 BernPoly 𝑋)
· (4 / 2))) |
| 207 | | 4d2e2 12436 |
. . . . . . . . 9
⊢ (4 / 2) =
2 |
| 208 | 207 | oveq2i 7442 |
. . . . . . . 8
⊢ ((3
BernPoly 𝑋) · (4 /
2)) = ((3 BernPoly 𝑋)
· 2) |
| 209 | 203, 191 | mulcomd 11282 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℂ → ((3
BernPoly 𝑋) · 2) =
(2 · (3 BernPoly 𝑋))) |
| 210 | | bpoly3 16094 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ → (3
BernPoly 𝑋) = (((𝑋↑3) − ((3 / 2)
· (𝑋↑2))) + ((1
/ 2) · 𝑋))) |
| 211 | 210 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℂ → (2
· (3 BernPoly 𝑋)) =
(2 · (((𝑋↑3)
− ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋)))) |
| 212 | 209, 211 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝑋 ∈ ℂ → ((3
BernPoly 𝑋) · 2) =
(2 · (((𝑋↑3)
− ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋)))) |
| 213 | 208, 212 | eqtrid 2789 |
. . . . . . 7
⊢ (𝑋 ∈ ℂ → ((3
BernPoly 𝑋) · (4 /
2)) = (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) ·
𝑋)))) |
| 214 | 206, 213 | eqtrd 2777 |
. . . . . 6
⊢ (𝑋 ∈ ℂ → (4
· ((3 BernPoly 𝑋) /
2)) = (2 · (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) ·
𝑋)))) |
| 215 | 200, 214 | oveq12d 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) · 𝑋))))) |
| 216 | 69, 215 | eqtrd 2777 |
. . . 4
⊢ (𝑋 ∈ ℂ →
Σ𝑘 ∈ (0...(2 +
1))((4C𝑘) · ((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = ((((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))) + (2 ·
(((𝑋↑3) − ((3 /
2) · (𝑋↑2))) +
((1 / 2) · 𝑋))))) |
| 217 | 8, 216 | eqtrid 2789 |
. . 3
⊢ (𝑋 ∈ ℂ →
Σ𝑘 ∈ (0...(4
− 1))((4C𝑘) ·
((𝑘 BernPoly 𝑋) / ((4 − 𝑘) + 1))) = ((((1 / 5) + (𝑋 − (1 / 2))) + (2 ·
(((𝑋↑2) − 𝑋) + (1 / 6)))) + (2 ·
(((𝑋↑3) − ((3 /
2) · (𝑋↑2))) +
((1 / 2) · 𝑋))))) |
| 218 | 217 | oveq2d 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) ∈ ℂ) |
| 220 | 1, 219 | mpan2 691 |
. . . 4
⊢ (𝑋 ∈ ℂ → (𝑋↑4) ∈
ℂ) |
| 221 | | expcl 14120 |
. . . . . 6
⊢ ((𝑋 ∈ ℂ ∧ 3 ∈
ℕ0) → (𝑋↑3) ∈ ℂ) |
| 222 | 201, 221 | mpan2 691 |
. . . . 5
⊢ (𝑋 ∈ ℂ → (𝑋↑3) ∈
ℂ) |
| 223 | 191, 222 | mulcld 11281 |
. . . 4
⊢ (𝑋 ∈ ℂ → (2
· (𝑋↑3)) ∈
ℂ) |
| 224 | | sqcl 14158 |
. . . . 5
⊢ (𝑋 ∈ ℂ → (𝑋↑2) ∈
ℂ) |
| 225 | 201, 100 | deccl 12748 |
. . . . . . . 8
⊢ ;30 ∈
ℕ0 |
| 226 | 225 | nn0cni 12538 |
. . . . . . 7
⊢ ;30 ∈ ℂ |
| 227 | | dfdec10 12736 |
. . . . . . . . 9
⊢ ;30 = ((;10 · 3) + 0) |
| 228 | | 10re 12752 |
. . . . . . . . . . . 12
⊢ ;10 ∈ ℝ |
| 229 | 228 | recni 11275 |
. . . . . . . . . . 11
⊢ ;10 ∈ ℂ |
| 230 | 229, 58 | mulcli 11268 |
. . . . . . . . . 10
⊢ (;10 · 3) ∈
ℂ |
| 231 | 230 | addridi 11448 |
. . . . . . . . 9
⊢ ((;10 · 3) + 0) = (;10 · 3) |
| 232 | 227, 231 | eqtri 2765 |
. . . . . . . 8
⊢ ;30 = (;10 · 3) |
| 233 | | 10pos 12750 |
. . . . . . . . . 10
⊢ 0 <
;10 |
| 234 | 136, 233 | gtneii 11373 |
. . . . . . . . 9
⊢ ;10 ≠ 0 |
| 235 | 229, 58, 234, 184 | mulne0i 11906 |
. . . . . . . 8
⊢ (;10 · 3) ≠ 0 |
| 236 | 232, 235 | eqnetri 3011 |
. . . . . . 7
⊢ ;30 ≠ 0 |
| 237 | 226, 236 | reccli 11997 |
. . . . . 6
⊢ (1 /
;30) ∈
ℂ |
| 238 | 237 | a1i 11 |
. . . . 5
⊢ (𝑋 ∈ ℂ → (1 /
;30) ∈
ℂ) |
| 239 | 224, 238 | subcld 11620 |
. . . 4
⊢ (𝑋 ∈ ℂ → ((𝑋↑2) − (1 / ;30)) ∈ ℂ) |
| 240 | 220, 223,
239 | subsubd 11648 |
. . 3
⊢ (𝑋 ∈ ℂ → ((𝑋↑4) − ((2 ·
(𝑋↑3)) − ((𝑋↑2) − (1 / ;30)))) = (((𝑋↑4) − (2 · (𝑋↑3))) + ((𝑋↑2) − (1 / ;30)))) |
| 241 | 161 | a1i 11 |
. . . . . . . 8
⊢ (𝑋 ∈ ℂ → (1 / 5)
∈ ℂ) |
| 242 | | id 22 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℂ → 𝑋 ∈
ℂ) |
| 243 | 87, 204 | reccli 11997 |
. . . . . . . . . 10
⊢ (1 / 2)
∈ ℂ |
| 244 | 243 | a1i 11 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℂ → (1 / 2)
∈ ℂ) |
| 245 | 242, 244 | subcld 11620 |
. . . . . . . 8
⊢ (𝑋 ∈ ℂ → (𝑋 − (1 / 2)) ∈
ℂ) |
| 246 | 241, 245 | addcld 11280 |
. . . . . . 7
⊢ (𝑋 ∈ ℂ → ((1 / 5)
+ (𝑋 − (1 / 2)))
∈ ℂ) |
| 247 | 224, 242 | subcld 11620 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℂ → ((𝑋↑2) − 𝑋) ∈
ℂ) |
| 248 | | 6pos 12376 |
. . . . . . . . . . . 12
⊢ 0 <
6 |
| 249 | 136, 248 | gtneii 11373 |
. . . . . . . . . . 11
⊢ 6 ≠
0 |
| 250 | 178, 249 | reccli 11997 |
. . . . . . . . . 10
⊢ (1 / 6)
∈ ℂ |
| 251 | 250 | a1i 11 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℂ → (1 / 6)
∈ ℂ) |
| 252 | 247, 251 | addcld 11280 |
. . . . . . . 8
⊢ (𝑋 ∈ ℂ → (((𝑋↑2) − 𝑋) + (1 / 6)) ∈
ℂ) |
| 253 | 191, 252 | mulcld 11281 |
. . . . . . 7
⊢ (𝑋 ∈ ℂ → (2
· (((𝑋↑2)
− 𝑋) + (1 / 6)))
∈ ℂ) |
| 254 | 246, 253 | addcld 11280 |
. . . . . 6
⊢ (𝑋 ∈ ℂ → (((1 / 5)
+ (𝑋 − (1 / 2))) + (2
· (((𝑋↑2)
− 𝑋) + (1 / 6))))
∈ ℂ) |
| 255 | 58, 87, 204 | divcli 12009 |
. . . . . . . . . . 11
⊢ (3 / 2)
∈ ℂ |
| 256 | 255 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ → (3 / 2)
∈ ℂ) |
| 257 | 256, 224 | mulcld 11281 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℂ → ((3 / 2)
· (𝑋↑2)) ∈
ℂ) |
| 258 | 222, 257 | subcld 11620 |
. . . . . . . 8
⊢ (𝑋 ∈ ℂ → ((𝑋↑3) − ((3 / 2)
· (𝑋↑2)))
∈ ℂ) |
| 259 | 244, 242 | mulcld 11281 |
. . . . . . . 8
⊢ (𝑋 ∈ ℂ → ((1 / 2)
· 𝑋) ∈
ℂ) |
| 260 | 258, 259 | addcld 11280 |
. . . . . . 7
⊢ (𝑋 ∈ ℂ → (((𝑋↑3) − ((3 / 2)
· (𝑋↑2))) + ((1
/ 2) · 𝑋)) ∈
ℂ) |
| 261 | 191, 260 | mulcld 11281 |
. . . . . 6
⊢ (𝑋 ∈ ℂ → (2
· (((𝑋↑3)
− ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))) ∈
ℂ) |
| 262 | 254, 261 | addcomd 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)))))) |
| 263 | 191, 258,
259 | adddid 11285 |
. . . . . . 7
⊢ (𝑋 ∈ ℂ → (2
· (((𝑋↑3)
− ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))) = ((2 · ((𝑋↑3) − ((3 / 2)
· (𝑋↑2)))) + (2
· ((1 / 2) · 𝑋)))) |
| 264 | 191, 222,
257 | subdid 11719 |
. . . . . . . 8
⊢ (𝑋 ∈ ℂ → (2
· ((𝑋↑3)
− ((3 / 2) · (𝑋↑2)))) = ((2 · (𝑋↑3)) − (2 ·
((3 / 2) · (𝑋↑2))))) |
| 265 | 87, 204 | recidi 11998 |
. . . . . . . . . 10
⊢ (2
· (1 / 2)) = 1 |
| 266 | 265 | oveq1i 7441 |
. . . . . . . . 9
⊢ ((2
· (1 / 2)) · 𝑋) = (1 · 𝑋) |
| 267 | 191, 244,
242 | mulassd 11284 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℂ → ((2
· (1 / 2)) · 𝑋) = (2 · ((1 / 2) · 𝑋))) |
| 268 | | mullid 11260 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℂ → (1
· 𝑋) = 𝑋) |
| 269 | 266, 267,
268 | 3eqtr3a 2801 |
. . . . . . . 8
⊢ (𝑋 ∈ ℂ → (2
· ((1 / 2) · 𝑋)) = 𝑋) |
| 270 | 264, 269 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑋 ∈ ℂ → ((2
· ((𝑋↑3)
− ((3 / 2) · (𝑋↑2)))) + (2 · ((1 / 2) ·
𝑋))) = (((2 · (𝑋↑3)) − (2 ·
((3 / 2) · (𝑋↑2)))) + 𝑋)) |
| 271 | 263, 270 | eqtrd 2777 |
. . . . . 6
⊢ (𝑋 ∈ ℂ → (2
· (((𝑋↑3)
− ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))) = (((2 · (𝑋↑3)) − (2 ·
((3 / 2) · (𝑋↑2)))) + 𝑋)) |
| 272 | 271 | oveq1d 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)))))) |
| 273 | 191, 257 | mulcld 11281 |
. . . . . . . 8
⊢ (𝑋 ∈ ℂ → (2
· ((3 / 2) · (𝑋↑2))) ∈ ℂ) |
| 274 | 223, 273 | subcld 11620 |
. . . . . . 7
⊢ (𝑋 ∈ ℂ → ((2
· (𝑋↑3))
− (2 · ((3 / 2) · (𝑋↑2)))) ∈ ℂ) |
| 275 | 274, 242,
254 | addassd 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))))))) |
| 276 | 242, 254 | addcld 11280 |
. . . . . . 7
⊢ (𝑋 ∈ ℂ → (𝑋 + (((1 / 5) + (𝑋 − (1 / 2))) + (2 ·
(((𝑋↑2) − 𝑋) + (1 / 6))))) ∈
ℂ) |
| 277 | 223, 273,
276 | subsubd 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))))))) |
| 278 | 191, 256,
224 | mulassd 11284 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ → ((2
· (3 / 2)) · (𝑋↑2)) = (2 · ((3 / 2) ·
(𝑋↑2)))) |
| 279 | 58, 87, 204 | divcan2i 12010 |
. . . . . . . . . . 11
⊢ (2
· (3 / 2)) = 3 |
| 280 | 279 | oveq1i 7441 |
. . . . . . . . . 10
⊢ ((2
· (3 / 2)) · (𝑋↑2)) = (3 · (𝑋↑2)) |
| 281 | 278, 280 | eqtr3di 2792 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℂ → (2
· ((3 / 2) · (𝑋↑2))) = (3 · (𝑋↑2))) |
| 282 | 281 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑋 ∈ ℂ → ((2
· ((3 / 2) · (𝑋↑2))) − (𝑋 + (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))))) = ((3 ·
(𝑋↑2)) − (𝑋 + (((1 / 5) + (𝑋 − (1 / 2))) + (2 ·
(((𝑋↑2) − 𝑋) + (1 /
6))))))) |
| 283 | 242, 246,
253 | add12d 11488 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ → (𝑋 + (((1 / 5) + (𝑋 − (1 / 2))) + (2 ·
(((𝑋↑2) − 𝑋) + (1 / 6))))) = (((1 / 5) +
(𝑋 − (1 / 2))) +
(𝑋 + (2 · (((𝑋↑2) − 𝑋) + (1 /
6)))))) |
| 284 | 191, 247,
251 | adddid 11285 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ ℂ → (2
· (((𝑋↑2)
− 𝑋) + (1 / 6))) =
((2 · ((𝑋↑2)
− 𝑋)) + (2 ·
(1 / 6)))) |
| 285 | 191, 224,
242 | subdid 11719 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 ∈ ℂ → (2
· ((𝑋↑2)
− 𝑋)) = ((2 ·
(𝑋↑2)) − (2
· 𝑋))) |
| 286 | 187 | oveq2i 7442 |
. . . . . . . . . . . . . . . . 17
⊢ (2 / (3
· 2)) = (2 / 6) |
| 287 | 58, 184 | reccli 11997 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1 / 3)
∈ ℂ |
| 288 | 58, 87, 287 | mul32i 11457 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((3
· 2) · (1 / 3)) = ((3 · (1 / 3)) ·
2) |
| 289 | 58, 184 | recidi 11998 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (3
· (1 / 3)) = 1 |
| 290 | 289 | oveq1i 7441 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((3
· (1 / 3)) · 2) = (1 · 2) |
| 291 | 87 | mullidi 11266 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1
· 2) = 2 |
| 292 | 290, 291 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((3
· (1 / 3)) · 2) = 2 |
| 293 | 288, 292 | eqtri 2765 |
. . . . . . . . . . . . . . . . . 18
⊢ ((3
· 2) · (1 / 3)) = 2 |
| 294 | 187, 178 | eqeltri 2837 |
. . . . . . . . . . . . . . . . . . 19
⊢ (3
· 2) ∈ ℂ |
| 295 | 187, 249 | eqnetri 3011 |
. . . . . . . . . . . . . . . . . . 19
⊢ (3
· 2) ≠ 0 |
| 296 | 87, 294, 287, 295 | divmuli 12021 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2 / (3
· 2)) = (1 / 3) ↔ ((3 · 2) · (1 / 3)) =
2) |
| 297 | 293, 296 | mpbir 231 |
. . . . . . . . . . . . . . . . 17
⊢ (2 / (3
· 2)) = (1 / 3) |
| 298 | 87, 178, 249 | divreci 12012 |
. . . . . . . . . . . . . . . . 17
⊢ (2 / 6) =
(2 · (1 / 6)) |
| 299 | 286, 297,
298 | 3eqtr3ri 2774 |
. . . . . . . . . . . . . . . 16
⊢ (2
· (1 / 6)) = (1 / 3) |
| 300 | 299 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 ∈ ℂ → (2
· (1 / 6)) = (1 / 3)) |
| 301 | 285, 300 | oveq12d 7449 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ ℂ → ((2
· ((𝑋↑2)
− 𝑋)) + (2 ·
(1 / 6))) = (((2 · (𝑋↑2)) − (2 · 𝑋)) + (1 / 3))) |
| 302 | 284, 301 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → (2
· (((𝑋↑2)
− 𝑋) + (1 / 6))) =
(((2 · (𝑋↑2))
− (2 · 𝑋)) +
(1 / 3))) |
| 303 | 302 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → (𝑋 + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))) = (𝑋 + (((2 · (𝑋↑2)) − (2 ·
𝑋)) + (1 /
3)))) |
| 304 | 191, 224 | mulcld 11281 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ ℂ → (2
· (𝑋↑2)) ∈
ℂ) |
| 305 | 191, 242 | mulcld 11281 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ ℂ → (2
· 𝑋) ∈
ℂ) |
| 306 | 304, 305 | subcld 11620 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → ((2
· (𝑋↑2))
− (2 · 𝑋))
∈ ℂ) |
| 307 | 287 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → (1 / 3)
∈ ℂ) |
| 308 | 242, 306,
307 | addassd 11283 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → ((𝑋 + ((2 · (𝑋↑2)) − (2 ·
𝑋))) + (1 / 3)) = (𝑋 + (((2 · (𝑋↑2)) − (2 ·
𝑋)) + (1 /
3)))) |
| 309 | 242, 304,
305 | addsub12d 11643 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → (𝑋 + ((2 · (𝑋↑2)) − (2 ·
𝑋))) = ((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋)))) |
| 310 | 309 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → ((𝑋 + ((2 · (𝑋↑2)) − (2 ·
𝑋))) + (1 / 3)) = (((2
· (𝑋↑2)) +
(𝑋 − (2 ·
𝑋))) + (1 /
3))) |
| 311 | 303, 308,
310 | 3eqtr2d 2783 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → (𝑋 + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))) = (((2 ·
(𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3))) |
| 312 | 311 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ → (((1 / 5)
+ (𝑋 − (1 / 2))) +
(𝑋 + (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))) = (((1 / 5) +
(𝑋 − (1 / 2))) + (((2
· (𝑋↑2)) +
(𝑋 − (2 ·
𝑋))) + (1 /
3)))) |
| 313 | 283, 312 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℂ → (𝑋 + (((1 / 5) + (𝑋 − (1 / 2))) + (2 ·
(((𝑋↑2) − 𝑋) + (1 / 6))))) = (((1 / 5) +
(𝑋 − (1 / 2))) + (((2
· (𝑋↑2)) +
(𝑋 − (2 ·
𝑋))) + (1 /
3)))) |
| 314 | 313 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑋 ∈ ℂ → ((3
· (𝑋↑2))
− (𝑋 + (((1 / 5) +
(𝑋 − (1 / 2))) + (2
· (((𝑋↑2)
− 𝑋) + (1 / 6)))))) =
((3 · (𝑋↑2))
− (((1 / 5) + (𝑋
− (1 / 2))) + (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3))))) |
| 315 | 242, 305 | subcld 11620 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → (𝑋 − (2 · 𝑋)) ∈
ℂ) |
| 316 | 304, 315 | addcld 11280 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → ((2
· (𝑋↑2)) +
(𝑋 − (2 ·
𝑋))) ∈
ℂ) |
| 317 | 241, 245,
316, 307 | add4d 11490 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → (((1 / 5)
+ (𝑋 − (1 / 2))) +
(((2 · (𝑋↑2)) +
(𝑋 − (2 ·
𝑋))) + (1 / 3))) = (((1 /
5) + ((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋)))) + ((𝑋 − (1 / 2)) + (1 /
3)))) |
| 318 | 241, 304,
315 | add12d 11488 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → ((1 / 5)
+ ((2 · (𝑋↑2))
+ (𝑋 − (2 ·
𝑋)))) = ((2 · (𝑋↑2)) + ((1 / 5) + (𝑋 − (2 · 𝑋))))) |
| 319 | 318 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → (((1 / 5)
+ ((2 · (𝑋↑2))
+ (𝑋 − (2 ·
𝑋)))) + ((𝑋 − (1 / 2)) + (1 / 3))) = (((2
· (𝑋↑2)) + ((1
/ 5) + (𝑋 − (2
· 𝑋)))) + ((𝑋 − (1 / 2)) + (1 /
3)))) |
| 320 | 241, 315 | addcld 11280 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → ((1 / 5)
+ (𝑋 − (2 ·
𝑋))) ∈
ℂ) |
| 321 | 245, 307 | addcld 11280 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → ((𝑋 − (1 / 2)) + (1 / 3))
∈ ℂ) |
| 322 | 304, 320,
321 | addassd 11283 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → (((2
· (𝑋↑2)) + ((1
/ 5) + (𝑋 − (2
· 𝑋)))) + ((𝑋 − (1 / 2)) + (1 / 3))) =
((2 · (𝑋↑2)) +
(((1 / 5) + (𝑋 − (2
· 𝑋))) + ((𝑋 − (1 / 2)) + (1 /
3))))) |
| 323 | 317, 319,
322 | 3eqtrd 2781 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ → (((1 / 5)
+ (𝑋 − (1 / 2))) +
(((2 · (𝑋↑2)) +
(𝑋 − (2 ·
𝑋))) + (1 / 3))) = ((2
· (𝑋↑2)) + (((1
/ 5) + (𝑋 − (2
· 𝑋))) + ((𝑋 − (1 / 2)) + (1 /
3))))) |
| 324 | 323 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℂ → ((3
· (𝑋↑2))
− (((1 / 5) + (𝑋
− (1 / 2))) + (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3)))) = ((3 · (𝑋↑2)) − ((2 ·
(𝑋↑2)) + (((1 / 5) +
(𝑋 − (2 ·
𝑋))) + ((𝑋 − (1 / 2)) + (1 /
3)))))) |
| 325 | 183, 224 | mulcld 11281 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ → (3
· (𝑋↑2)) ∈
ℂ) |
| 326 | 320, 321 | addcld 11280 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ → (((1 / 5)
+ (𝑋 − (2 ·
𝑋))) + ((𝑋 − (1 / 2)) + (1 / 3))) ∈
ℂ) |
| 327 | 325, 304,
326 | subsub4d 11651 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℂ → (((3
· (𝑋↑2))
− (2 · (𝑋↑2))) − (((1 / 5) + (𝑋 − (2 · 𝑋))) + ((𝑋 − (1 / 2)) + (1 / 3)))) = ((3
· (𝑋↑2))
− ((2 · (𝑋↑2)) + (((1 / 5) + (𝑋 − (2 · 𝑋))) + ((𝑋 − (1 / 2)) + (1 /
3)))))) |
| 328 | 58, 87, 59, 109 | subaddrii 11598 |
. . . . . . . . . . . 12
⊢ (3
− 2) = 1 |
| 329 | 328 | oveq1i 7441 |
. . . . . . . . . . 11
⊢ ((3
− 2) · (𝑋↑2)) = (1 · (𝑋↑2)) |
| 330 | 183, 191,
224 | subdird 11720 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → ((3
− 2) · (𝑋↑2)) = ((3 · (𝑋↑2)) − (2 · (𝑋↑2)))) |
| 331 | 224 | mullidd 11279 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → (1
· (𝑋↑2)) =
(𝑋↑2)) |
| 332 | 329, 330,
331 | 3eqtr3a 2801 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ → ((3
· (𝑋↑2))
− (2 · (𝑋↑2))) = (𝑋↑2)) |
| 333 | 241, 305,
242 | subsubd 11648 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → ((1 / 5)
− ((2 · 𝑋)
− 𝑋)) = (((1 / 5)
− (2 · 𝑋)) +
𝑋)) |
| 334 | | 2txmxeqx 12406 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ ℂ → ((2
· 𝑋) − 𝑋) = 𝑋) |
| 335 | 334 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → ((1 / 5)
− ((2 · 𝑋)
− 𝑋)) = ((1 / 5)
− 𝑋)) |
| 336 | 241, 305,
242 | subadd23d 11642 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → (((1 / 5)
− (2 · 𝑋)) +
𝑋) = ((1 / 5) + (𝑋 − (2 · 𝑋)))) |
| 337 | 333, 335,
336 | 3eqtr3d 2785 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → ((1 / 5)
− 𝑋) = ((1 / 5) +
(𝑋 − (2 ·
𝑋)))) |
| 338 | 242, 244,
307 | subsubd 11648 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → (𝑋 − ((1 / 2) − (1 /
3))) = ((𝑋 − (1 / 2))
+ (1 / 3))) |
| 339 | 337, 338 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → (((1 / 5)
− 𝑋) + (𝑋 − ((1 / 2) − (1 /
3)))) = (((1 / 5) + (𝑋
− (2 · 𝑋))) +
((𝑋 − (1 / 2)) + (1 /
3)))) |
| 340 | 243, 287 | subcli 11585 |
. . . . . . . . . . . . . 14
⊢ ((1 / 2)
− (1 / 3)) ∈ ℂ |
| 341 | 340 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → ((1 / 2)
− (1 / 3)) ∈ ℂ) |
| 342 | 241, 242,
341 | npncand 11644 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → (((1 / 5)
− 𝑋) + (𝑋 − ((1 / 2) − (1 /
3)))) = ((1 / 5) − ((1 / 2) − (1 / 3)))) |
| 343 | | halfthird 12876 |
. . . . . . . . . . . . . 14
⊢ ((1 / 2)
− (1 / 3)) = (1 / 6) |
| 344 | 343 | oveq2i 7442 |
. . . . . . . . . . . . 13
⊢ ((1 / 5)
− ((1 / 2) − (1 / 3))) = ((1 / 5) − (1 / 6)) |
| 345 | | 5recm6rec 12877 |
. . . . . . . . . . . . 13
⊢ ((1 / 5)
− (1 / 6)) = (1 / ;30) |
| 346 | 344, 345 | eqtri 2765 |
. . . . . . . . . . . 12
⊢ ((1 / 5)
− ((1 / 2) − (1 / 3))) = (1 / ;30) |
| 347 | 342, 346 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → (((1 / 5)
− 𝑋) + (𝑋 − ((1 / 2) − (1 /
3)))) = (1 / ;30)) |
| 348 | 339, 347 | eqtr3d 2779 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ → (((1 / 5)
+ (𝑋 − (2 ·
𝑋))) + ((𝑋 − (1 / 2)) + (1 / 3))) = (1 / ;30)) |
| 349 | 332, 348 | oveq12d 7449 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℂ → (((3
· (𝑋↑2))
− (2 · (𝑋↑2))) − (((1 / 5) + (𝑋 − (2 · 𝑋))) + ((𝑋 − (1 / 2)) + (1 / 3)))) = ((𝑋↑2) − (1 / ;30))) |
| 350 | 324, 327,
349 | 3eqtr2d 2783 |
. . . . . . . 8
⊢ (𝑋 ∈ ℂ → ((3
· (𝑋↑2))
− (((1 / 5) + (𝑋
− (1 / 2))) + (((2 · (𝑋↑2)) + (𝑋 − (2 · 𝑋))) + (1 / 3)))) = ((𝑋↑2) − (1 / ;30))) |
| 351 | 282, 314,
350 | 3eqtrd 2781 |
. . . . . . 7
⊢ (𝑋 ∈ ℂ → ((2
· ((3 / 2) · (𝑋↑2))) − (𝑋 + (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6)))))) = ((𝑋↑2) − (1 / ;30))) |
| 352 | 351 | oveq2d 7447 |
. . . . . 6
⊢ (𝑋 ∈ ℂ → ((2
· (𝑋↑3))
− ((2 · ((3 / 2) · (𝑋↑2))) − (𝑋 + (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))))) = ((2 ·
(𝑋↑3)) − ((𝑋↑2) − (1 / ;30)))) |
| 353 | 275, 277,
352 | 3eqtr2d 2783 |
. . . . 5
⊢ (𝑋 ∈ ℂ → ((((2
· (𝑋↑3))
− (2 · ((3 / 2) · (𝑋↑2)))) + 𝑋) + (((1 / 5) + (𝑋 − (1 / 2))) + (2 · (((𝑋↑2) − 𝑋) + (1 / 6))))) = ((2 ·
(𝑋↑3)) − ((𝑋↑2) − (1 / ;30)))) |
| 354 | 262, 272,
353 | 3eqtrd 2781 |
. . . 4
⊢ (𝑋 ∈ ℂ → ((((1 /
5) + (𝑋 − (1 / 2))) +
(2 · (((𝑋↑2)
− 𝑋) + (1 / 6)))) +
(2 · (((𝑋↑3)
− ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋)))) = ((2 · (𝑋↑3)) − ((𝑋↑2) − (1 / ;30)))) |
| 355 | 354 | oveq2d 7447 |
. . 3
⊢ (𝑋 ∈ ℂ → ((𝑋↑4) − ((((1 / 5) +
(𝑋 − (1 / 2))) + (2
· (((𝑋↑2)
− 𝑋) + (1 / 6)))) +
(2 · (((𝑋↑3)
− ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))))) = ((𝑋↑4) − ((2 · (𝑋↑3)) − ((𝑋↑2) − (1 / ;30))))) |
| 356 | 220, 223 | subcld 11620 |
. . . 4
⊢ (𝑋 ∈ ℂ → ((𝑋↑4) − (2 ·
(𝑋↑3))) ∈
ℂ) |
| 357 | 356, 224,
238 | addsubassd 11640 |
. . 3
⊢ (𝑋 ∈ ℂ → ((((𝑋↑4) − (2 ·
(𝑋↑3))) + (𝑋↑2)) − (1 / ;30)) = (((𝑋↑4) − (2 · (𝑋↑3))) + ((𝑋↑2) − (1 / ;30)))) |
| 358 | 240, 355,
357 | 3eqtr4d 2787 |
. 2
⊢ (𝑋 ∈ ℂ → ((𝑋↑4) − ((((1 / 5) +
(𝑋 − (1 / 2))) + (2
· (((𝑋↑2)
− 𝑋) + (1 / 6)))) +
(2 · (((𝑋↑3)
− ((3 / 2) · (𝑋↑2))) + ((1 / 2) · 𝑋))))) = ((((𝑋↑4) − (2 · (𝑋↑3))) + (𝑋↑2)) − (1 / ;30))) |
| 359 | 3, 218, 358 | 3eqtrd 2781 |
1
⊢ (𝑋 ∈ ℂ → (4
BernPoly 𝑋) = ((((𝑋↑4) − (2 ·
(𝑋↑3))) + (𝑋↑2)) − (1 / ;30))) |