| Step | Hyp | Ref
| Expression |
| 1 | | 3nn0 12544 |
. . 3
⊢ 3 ∈
ℕ0 |
| 2 | | bpolyval 16085 |
. . 3
⊢ ((3
∈ ℕ0 ∧ 𝑋 ∈ ℂ) → (3 BernPoly 𝑋) = ((𝑋↑3) − Σ𝑘 ∈ (0...(3 − 1))((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))))) |
| 3 | 1, 2 | mpan 690 |
. 2
⊢ (𝑋 ∈ ℂ → (3
BernPoly 𝑋) = ((𝑋↑3) − Σ𝑘 ∈ (0...(3 −
1))((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))))) |
| 4 | | 3m1e2 12394 |
. . . . . . 7
⊢ (3
− 1) = 2 |
| 5 | | df-2 12329 |
. . . . . . 7
⊢ 2 = (1 +
1) |
| 6 | 4, 5 | eqtri 2765 |
. . . . . 6
⊢ (3
− 1) = (1 + 1) |
| 7 | 6 | oveq2i 7442 |
. . . . 5
⊢ (0...(3
− 1)) = (0...(1 + 1)) |
| 8 | 7 | sumeq1i 15733 |
. . . 4
⊢
Σ𝑘 ∈
(0...(3 − 1))((3C𝑘)
· ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = Σ𝑘 ∈ (0...(1 + 1))((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) |
| 9 | | 1eluzge0 12934 |
. . . . . . 7
⊢ 1 ∈
(ℤ≥‘0) |
| 10 | 9 | a1i 11 |
. . . . . 6
⊢ (𝑋 ∈ ℂ → 1 ∈
(ℤ≥‘0)) |
| 11 | | 0z 12624 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℤ |
| 12 | | fzpr 13619 |
. . . . . . . . . . . . 13
⊢ (0 ∈
ℤ → (0...(0 + 1)) = {0, (0 + 1)}) |
| 13 | 11, 12 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (0...(0 +
1)) = {0, (0 + 1)} |
| 14 | | 0p1e1 12388 |
. . . . . . . . . . . . 13
⊢ (0 + 1) =
1 |
| 15 | 14 | oveq2i 7442 |
. . . . . . . . . . . 12
⊢ (0...(0 +
1)) = (0...1) |
| 16 | 14 | preq2i 4737 |
. . . . . . . . . . . 12
⊢ {0, (0 +
1)} = {0, 1} |
| 17 | 13, 15, 16 | 3eqtr3ri 2774 |
. . . . . . . . . . 11
⊢ {0, 1} =
(0...1) |
| 18 | 5 | sneqi 4637 |
. . . . . . . . . . 11
⊢ {2} = {(1
+ 1)} |
| 19 | 17, 18 | uneq12i 4166 |
. . . . . . . . . 10
⊢ ({0, 1}
∪ {2}) = ((0...1) ∪ {(1 + 1)}) |
| 20 | | df-tp 4631 |
. . . . . . . . . 10
⊢ {0, 1, 2}
= ({0, 1} ∪ {2}) |
| 21 | | fzsuc 13611 |
. . . . . . . . . . 11
⊢ (1 ∈
(ℤ≥‘0) → (0...(1 + 1)) = ((0...1) ∪ {(1 +
1)})) |
| 22 | 9, 21 | ax-mp 5 |
. . . . . . . . . 10
⊢ (0...(1 +
1)) = ((0...1) ∪ {(1 + 1)}) |
| 23 | 19, 20, 22 | 3eqtr4ri 2776 |
. . . . . . . . 9
⊢ (0...(1 +
1)) = {0, 1, 2} |
| 24 | 23 | eleq2i 2833 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...(1 + 1)) ↔
𝑘 ∈ {0, 1,
2}) |
| 25 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑘 ∈ V |
| 26 | 25 | eltp 4689 |
. . . . . . . 8
⊢ (𝑘 ∈ {0, 1, 2} ↔ (𝑘 = 0 ∨ 𝑘 = 1 ∨ 𝑘 = 2)) |
| 27 | 24, 26 | bitri 275 |
. . . . . . 7
⊢ (𝑘 ∈ (0...(1 + 1)) ↔
(𝑘 = 0 ∨ 𝑘 = 1 ∨ 𝑘 = 2)) |
| 28 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑘 = 0 → (3C𝑘) = (3C0)) |
| 29 | | bcn0 14349 |
. . . . . . . . . . . . 13
⊢ (3 ∈
ℕ0 → (3C0) = 1) |
| 30 | 1, 29 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (3C0) =
1 |
| 31 | 28, 30 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (𝑘 = 0 → (3C𝑘) = 1) |
| 32 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑘 = 0 → (𝑘 BernPoly 𝑋) = (0 BernPoly 𝑋)) |
| 33 | | oveq2 7439 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 0 → (3 − 𝑘) = (3 −
0)) |
| 34 | 33 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 0 → ((3 − 𝑘) + 1) = ((3 − 0) +
1)) |
| 35 | | 3cn 12347 |
. . . . . . . . . . . . . . . 16
⊢ 3 ∈
ℂ |
| 36 | 35 | subid1i 11581 |
. . . . . . . . . . . . . . 15
⊢ (3
− 0) = 3 |
| 37 | 36 | oveq1i 7441 |
. . . . . . . . . . . . . 14
⊢ ((3
− 0) + 1) = (3 + 1) |
| 38 | | df-4 12331 |
. . . . . . . . . . . . . 14
⊢ 4 = (3 +
1) |
| 39 | 37, 38 | eqtr4i 2768 |
. . . . . . . . . . . . 13
⊢ ((3
− 0) + 1) = 4 |
| 40 | 34, 39 | eqtrdi 2793 |
. . . . . . . . . . . 12
⊢ (𝑘 = 0 → ((3 − 𝑘) + 1) = 4) |
| 41 | 32, 40 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (𝑘 = 0 → ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1)) = ((0 BernPoly 𝑋) / 4)) |
| 42 | 31, 41 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝑘 = 0 → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (1 · ((0 BernPoly 𝑋) / 4))) |
| 43 | | bpoly0 16086 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → (0
BernPoly 𝑋) =
1) |
| 44 | 43 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → ((0
BernPoly 𝑋) / 4) = (1 /
4)) |
| 45 | 44 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → (1
· ((0 BernPoly 𝑋) /
4)) = (1 · (1 / 4))) |
| 46 | | 4cn 12351 |
. . . . . . . . . . . . 13
⊢ 4 ∈
ℂ |
| 47 | | 4ne0 12374 |
. . . . . . . . . . . . 13
⊢ 4 ≠
0 |
| 48 | 46, 47 | reccli 11997 |
. . . . . . . . . . . 12
⊢ (1 / 4)
∈ ℂ |
| 49 | 48 | mullidi 11266 |
. . . . . . . . . . 11
⊢ (1
· (1 / 4)) = (1 / 4) |
| 50 | 45, 49 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ → (1
· ((0 BernPoly 𝑋) /
4)) = (1 / 4)) |
| 51 | 42, 50 | sylan9eqr 2799 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 = 0) → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (1 / 4)) |
| 52 | 51, 48 | eqeltrdi 2849 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 = 0) → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) ∈ ℂ) |
| 53 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑘 = 1 → (3C𝑘) = (3C1)) |
| 54 | | bcn1 14352 |
. . . . . . . . . . . . 13
⊢ (3 ∈
ℕ0 → (3C1) = 3) |
| 55 | 1, 54 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (3C1) =
3 |
| 56 | 53, 55 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (𝑘 = 1 → (3C𝑘) = 3) |
| 57 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑘 = 1 → (𝑘 BernPoly 𝑋) = (1 BernPoly 𝑋)) |
| 58 | | oveq2 7439 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 1 → (3 − 𝑘) = (3 −
1)) |
| 59 | 58 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 1 → ((3 − 𝑘) + 1) = ((3 − 1) +
1)) |
| 60 | | ax-1cn 11213 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℂ |
| 61 | | npcan 11517 |
. . . . . . . . . . . . . 14
⊢ ((3
∈ ℂ ∧ 1 ∈ ℂ) → ((3 − 1) + 1) =
3) |
| 62 | 35, 60, 61 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ ((3
− 1) + 1) = 3 |
| 63 | 59, 62 | eqtrdi 2793 |
. . . . . . . . . . . 12
⊢ (𝑘 = 1 → ((3 − 𝑘) + 1) = 3) |
| 64 | 57, 63 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (𝑘 = 1 → ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1)) = ((1 BernPoly 𝑋) / 3)) |
| 65 | 56, 64 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝑘 = 1 → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (3 · ((1 BernPoly 𝑋) / 3))) |
| 66 | | bpoly1 16087 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → (1
BernPoly 𝑋) = (𝑋 − (1 /
2))) |
| 67 | 66 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → ((1
BernPoly 𝑋) / 3) = ((𝑋 − (1 / 2)) /
3)) |
| 68 | 67 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → (3
· ((1 BernPoly 𝑋) /
3)) = (3 · ((𝑋
− (1 / 2)) / 3))) |
| 69 | | halfcn 12481 |
. . . . . . . . . . . . 13
⊢ (1 / 2)
∈ ℂ |
| 70 | | subcl 11507 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ ℂ ∧ (1 / 2)
∈ ℂ) → (𝑋
− (1 / 2)) ∈ ℂ) |
| 71 | 69, 70 | mpan2 691 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → (𝑋 − (1 / 2)) ∈
ℂ) |
| 72 | | 3ne0 12372 |
. . . . . . . . . . . . 13
⊢ 3 ≠
0 |
| 73 | | divcan2 11930 |
. . . . . . . . . . . . 13
⊢ (((𝑋 − (1 / 2)) ∈ ℂ
∧ 3 ∈ ℂ ∧ 3 ≠ 0) → (3 · ((𝑋 − (1 / 2)) / 3)) = (𝑋 − (1 / 2))) |
| 74 | 35, 72, 73 | mp3an23 1455 |
. . . . . . . . . . . 12
⊢ ((𝑋 − (1 / 2)) ∈ ℂ
→ (3 · ((𝑋
− (1 / 2)) / 3)) = (𝑋
− (1 / 2))) |
| 75 | 71, 74 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → (3
· ((𝑋 − (1 /
2)) / 3)) = (𝑋 − (1 /
2))) |
| 76 | 68, 75 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ → (3
· ((1 BernPoly 𝑋) /
3)) = (𝑋 − (1 /
2))) |
| 77 | 65, 76 | sylan9eqr 2799 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 = 1) → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (𝑋 − (1 / 2))) |
| 78 | 71 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 = 1) → (𝑋 − (1 / 2)) ∈
ℂ) |
| 79 | 77, 78 | eqeltrd 2841 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 = 1) → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) ∈ ℂ) |
| 80 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑘 = 2 → (3C𝑘) = (3C2)) |
| 81 | | bcn2 14358 |
. . . . . . . . . . . . . 14
⊢ (3 ∈
ℕ0 → (3C2) = ((3 · (3 − 1)) /
2)) |
| 82 | 1, 81 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (3C2) =
((3 · (3 − 1)) / 2) |
| 83 | 4 | oveq2i 7442 |
. . . . . . . . . . . . . . 15
⊢ (3
· (3 − 1)) = (3 · 2) |
| 84 | 83 | oveq1i 7441 |
. . . . . . . . . . . . . 14
⊢ ((3
· (3 − 1)) / 2) = ((3 · 2) / 2) |
| 85 | | 2cn 12341 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℂ |
| 86 | | 2ne0 12370 |
. . . . . . . . . . . . . . 15
⊢ 2 ≠
0 |
| 87 | 35, 85, 86 | divcan4i 12014 |
. . . . . . . . . . . . . 14
⊢ ((3
· 2) / 2) = 3 |
| 88 | 84, 87 | eqtri 2765 |
. . . . . . . . . . . . 13
⊢ ((3
· (3 − 1)) / 2) = 3 |
| 89 | 82, 88 | eqtri 2765 |
. . . . . . . . . . . 12
⊢ (3C2) =
3 |
| 90 | 80, 89 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (𝑘 = 2 → (3C𝑘) = 3) |
| 91 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑘 = 2 → (𝑘 BernPoly 𝑋) = (2 BernPoly 𝑋)) |
| 92 | | oveq2 7439 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 2 → (3 − 𝑘) = (3 −
2)) |
| 93 | 92 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 2 → ((3 − 𝑘) + 1) = ((3 − 2) +
1)) |
| 94 | | 2p1e3 12408 |
. . . . . . . . . . . . . . . 16
⊢ (2 + 1) =
3 |
| 95 | 35, 85, 60, 94 | subaddrii 11598 |
. . . . . . . . . . . . . . 15
⊢ (3
− 2) = 1 |
| 96 | 95 | oveq1i 7441 |
. . . . . . . . . . . . . 14
⊢ ((3
− 2) + 1) = (1 + 1) |
| 97 | 96, 5 | eqtr4i 2768 |
. . . . . . . . . . . . 13
⊢ ((3
− 2) + 1) = 2 |
| 98 | 93, 97 | eqtrdi 2793 |
. . . . . . . . . . . 12
⊢ (𝑘 = 2 → ((3 − 𝑘) + 1) = 2) |
| 99 | 91, 98 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (𝑘 = 2 → ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1)) = ((2 BernPoly 𝑋) / 2)) |
| 100 | 90, 99 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝑘 = 2 → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (3 · ((2 BernPoly 𝑋) / 2))) |
| 101 | | 2nn0 12543 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ0 |
| 102 | | bpolycl 16088 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℕ0 ∧ 𝑋 ∈ ℂ) → (2 BernPoly 𝑋) ∈
ℂ) |
| 103 | 101, 102 | mpan 690 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → (2
BernPoly 𝑋) ∈
ℂ) |
| 104 | | 2cnne0 12476 |
. . . . . . . . . . . . 13
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
| 105 | | div12 11944 |
. . . . . . . . . . . . 13
⊢ ((3
∈ ℂ ∧ (2 BernPoly 𝑋) ∈ ℂ ∧ (2 ∈ ℂ
∧ 2 ≠ 0)) → (3 · ((2 BernPoly 𝑋) / 2)) = ((2 BernPoly 𝑋) · (3 / 2))) |
| 106 | 35, 104, 105 | mp3an13 1454 |
. . . . . . . . . . . 12
⊢ ((2
BernPoly 𝑋) ∈ ℂ
→ (3 · ((2 BernPoly 𝑋) / 2)) = ((2 BernPoly 𝑋) · (3 / 2))) |
| 107 | 103, 106 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → (3
· ((2 BernPoly 𝑋) /
2)) = ((2 BernPoly 𝑋)
· (3 / 2))) |
| 108 | 35, 85, 86 | divcli 12009 |
. . . . . . . . . . . 12
⊢ (3 / 2)
∈ ℂ |
| 109 | | mulcom 11241 |
. . . . . . . . . . . 12
⊢ (((2
BernPoly 𝑋) ∈ ℂ
∧ (3 / 2) ∈ ℂ) → ((2 BernPoly 𝑋) · (3 / 2)) = ((3 / 2) · (2
BernPoly 𝑋))) |
| 110 | 103, 108,
109 | sylancl 586 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → ((2
BernPoly 𝑋) · (3 /
2)) = ((3 / 2) · (2 BernPoly 𝑋))) |
| 111 | | bpoly2 16093 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → (2
BernPoly 𝑋) = (((𝑋↑2) − 𝑋) + (1 / 6))) |
| 112 | 111 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → ((3 / 2)
· (2 BernPoly 𝑋)) =
((3 / 2) · (((𝑋↑2) − 𝑋) + (1 / 6)))) |
| 113 | | sqcl 14158 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ ℂ → (𝑋↑2) ∈
ℂ) |
| 114 | | 6cn 12357 |
. . . . . . . . . . . . . . . 16
⊢ 6 ∈
ℂ |
| 115 | | 6re 12356 |
. . . . . . . . . . . . . . . . 17
⊢ 6 ∈
ℝ |
| 116 | | 6pos 12376 |
. . . . . . . . . . . . . . . . 17
⊢ 0 <
6 |
| 117 | 115, 116 | gt0ne0ii 11799 |
. . . . . . . . . . . . . . . 16
⊢ 6 ≠
0 |
| 118 | 114, 117 | reccli 11997 |
. . . . . . . . . . . . . . 15
⊢ (1 / 6)
∈ ℂ |
| 119 | | subsub 11539 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋↑2) ∈ ℂ ∧
𝑋 ∈ ℂ ∧ (1 /
6) ∈ ℂ) → ((𝑋↑2) − (𝑋 − (1 / 6))) = (((𝑋↑2) − 𝑋) + (1 / 6))) |
| 120 | 118, 119 | mp3an3 1452 |
. . . . . . . . . . . . . 14
⊢ (((𝑋↑2) ∈ ℂ ∧
𝑋 ∈ ℂ) →
((𝑋↑2) − (𝑋 − (1 / 6))) = (((𝑋↑2) − 𝑋) + (1 / 6))) |
| 121 | 113, 120 | mpancom 688 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → ((𝑋↑2) − (𝑋 − (1 / 6))) = (((𝑋↑2) − 𝑋) + (1 / 6))) |
| 122 | 121 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → ((3 / 2)
· ((𝑋↑2)
− (𝑋 − (1 /
6)))) = ((3 / 2) · (((𝑋↑2) − 𝑋) + (1 / 6)))) |
| 123 | | subcl 11507 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ ℂ ∧ (1 / 6)
∈ ℂ) → (𝑋
− (1 / 6)) ∈ ℂ) |
| 124 | 118, 123 | mpan2 691 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → (𝑋 − (1 / 6)) ∈
ℂ) |
| 125 | | subdi 11696 |
. . . . . . . . . . . . 13
⊢ (((3 / 2)
∈ ℂ ∧ (𝑋↑2) ∈ ℂ ∧ (𝑋 − (1 / 6)) ∈
ℂ) → ((3 / 2) · ((𝑋↑2) − (𝑋 − (1 / 6)))) = (((3 / 2) ·
(𝑋↑2)) − ((3 /
2) · (𝑋 − (1 /
6))))) |
| 126 | 108, 113,
124, 125 | mp3an2i 1468 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → ((3 / 2)
· ((𝑋↑2)
− (𝑋 − (1 /
6)))) = (((3 / 2) · (𝑋↑2)) − ((3 / 2) · (𝑋 − (1 /
6))))) |
| 127 | 112, 122,
126 | 3eqtr2d 2783 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → ((3 / 2)
· (2 BernPoly 𝑋)) =
(((3 / 2) · (𝑋↑2)) − ((3 / 2) · (𝑋 − (1 /
6))))) |
| 128 | 107, 110,
127 | 3eqtrd 2781 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ → (3
· ((2 BernPoly 𝑋) /
2)) = (((3 / 2) · (𝑋↑2)) − ((3 / 2) · (𝑋 − (1 /
6))))) |
| 129 | 100, 128 | sylan9eqr 2799 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 = 2) → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (((3 / 2) · (𝑋↑2)) − ((3 / 2)
· (𝑋 − (1 /
6))))) |
| 130 | | mulcl 11239 |
. . . . . . . . . . . 12
⊢ (((3 / 2)
∈ ℂ ∧ (𝑋↑2) ∈ ℂ) → ((3 / 2)
· (𝑋↑2)) ∈
ℂ) |
| 131 | 108, 113,
130 | sylancr 587 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → ((3 / 2)
· (𝑋↑2)) ∈
ℂ) |
| 132 | | mulcl 11239 |
. . . . . . . . . . . 12
⊢ (((3 / 2)
∈ ℂ ∧ (𝑋
− (1 / 6)) ∈ ℂ) → ((3 / 2) · (𝑋 − (1 / 6))) ∈
ℂ) |
| 133 | 108, 124,
132 | sylancr 587 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → ((3 / 2)
· (𝑋 − (1 /
6))) ∈ ℂ) |
| 134 | 131, 133 | subcld 11620 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ → (((3 / 2)
· (𝑋↑2))
− ((3 / 2) · (𝑋 − (1 / 6)))) ∈
ℂ) |
| 135 | 134 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 = 2) → (((3 / 2) ·
(𝑋↑2)) − ((3 /
2) · (𝑋 − (1 /
6)))) ∈ ℂ) |
| 136 | 129, 135 | eqeltrd 2841 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 = 2) → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) ∈ ℂ) |
| 137 | 52, 79, 136 | 3jaodan 1433 |
. . . . . . 7
⊢ ((𝑋 ∈ ℂ ∧ (𝑘 = 0 ∨ 𝑘 = 1 ∨ 𝑘 = 2)) → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) ∈ ℂ) |
| 138 | 27, 137 | sylan2b 594 |
. . . . . 6
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(1 + 1))) →
((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) ∈ ℂ) |
| 139 | 5 | eqeq2i 2750 |
. . . . . . 7
⊢ (𝑘 = 2 ↔ 𝑘 = (1 + 1)) |
| 140 | 139, 100 | sylbir 235 |
. . . . . 6
⊢ (𝑘 = (1 + 1) → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (3 · ((2 BernPoly 𝑋) / 2))) |
| 141 | 10, 138, 140 | fsump1 15792 |
. . . . 5
⊢ (𝑋 ∈ ℂ →
Σ𝑘 ∈ (0...(1 +
1))((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (Σ𝑘 ∈ (0...1)((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) + (3 · ((2 BernPoly 𝑋) / 2)))) |
| 142 | 128 | oveq2d 7447 |
. . . . 5
⊢ (𝑋 ∈ ℂ →
(Σ𝑘 ∈
(0...1)((3C𝑘) ·
((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) + (3 · ((2
BernPoly 𝑋) / 2))) =
(Σ𝑘 ∈
(0...1)((3C𝑘) ·
((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) + (((3 / 2) ·
(𝑋↑2)) − ((3 /
2) · (𝑋 − (1 /
6)))))) |
| 143 | 15 | sumeq1i 15733 |
. . . . . . . . 9
⊢
Σ𝑘 ∈
(0...(0 + 1))((3C𝑘)
· ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = Σ𝑘 ∈ (0...1)((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) |
| 144 | | 0nn0 12541 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℕ0 |
| 145 | | nn0uz 12920 |
. . . . . . . . . . . . 13
⊢
ℕ0 = (ℤ≥‘0) |
| 146 | 144, 145 | eleqtri 2839 |
. . . . . . . . . . . 12
⊢ 0 ∈
(ℤ≥‘0) |
| 147 | 146 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → 0 ∈
(ℤ≥‘0)) |
| 148 | 13, 16 | eqtri 2765 |
. . . . . . . . . . . . . 14
⊢ (0...(0 +
1)) = {0, 1} |
| 149 | 148 | eleq2i 2833 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0...(0 + 1)) ↔
𝑘 ∈ {0,
1}) |
| 150 | 25 | elpr 4650 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ {0, 1} ↔ (𝑘 = 0 ∨ 𝑘 = 1)) |
| 151 | 149, 150 | bitri 275 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (0...(0 + 1)) ↔
(𝑘 = 0 ∨ 𝑘 = 1)) |
| 152 | 52, 79 | jaodan 960 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ ℂ ∧ (𝑘 = 0 ∨ 𝑘 = 1)) → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) ∈ ℂ) |
| 153 | 151, 152 | sylan2b 594 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(0 + 1))) →
((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) ∈ ℂ) |
| 154 | 14 | eqeq2i 2750 |
. . . . . . . . . . . 12
⊢ (𝑘 = (0 + 1) ↔ 𝑘 = 1) |
| 155 | 154, 65 | sylbi 217 |
. . . . . . . . . . 11
⊢ (𝑘 = (0 + 1) → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (3 · ((1 BernPoly 𝑋) / 3))) |
| 156 | 147, 153,
155 | fsump1 15792 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ →
Σ𝑘 ∈ (0...(0 +
1))((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (Σ𝑘 ∈ (0...0)((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) + (3 · ((1 BernPoly 𝑋) / 3)))) |
| 157 | 50, 48 | eqeltrdi 2849 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → (1
· ((0 BernPoly 𝑋) /
4)) ∈ ℂ) |
| 158 | 42 | fsum1 15783 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℤ ∧ (1 · ((0 BernPoly 𝑋) / 4)) ∈ ℂ) → Σ𝑘 ∈ (0...0)((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (1 · ((0 BernPoly 𝑋) / 4))) |
| 159 | 11, 157, 158 | sylancr 587 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ →
Σ𝑘 ∈
(0...0)((3C𝑘) ·
((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (1 · ((0
BernPoly 𝑋) /
4))) |
| 160 | 159, 50 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ →
Σ𝑘 ∈
(0...0)((3C𝑘) ·
((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (1 /
4)) |
| 161 | 160, 76 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ →
(Σ𝑘 ∈
(0...0)((3C𝑘) ·
((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) + (3 · ((1
BernPoly 𝑋) / 3))) = ((1 /
4) + (𝑋 − (1 /
2)))) |
| 162 | 156, 161 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℂ →
Σ𝑘 ∈ (0...(0 +
1))((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = ((1 / 4) + (𝑋 − (1 / 2)))) |
| 163 | 143, 162 | eqtr3id 2791 |
. . . . . . . 8
⊢ (𝑋 ∈ ℂ →
Σ𝑘 ∈
(0...1)((3C𝑘) ·
((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = ((1 / 4) + (𝑋 − (1 /
2)))) |
| 164 | 163 | oveq1d 7446 |
. . . . . . 7
⊢ (𝑋 ∈ ℂ →
(Σ𝑘 ∈
(0...1)((3C𝑘) ·
((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) + (((3 / 2) ·
(𝑋↑2)) − ((3 /
2) · (𝑋 − (1 /
6))))) = (((1 / 4) + (𝑋
− (1 / 2))) + (((3 / 2) · (𝑋↑2)) − ((3 / 2) · (𝑋 − (1 /
6)))))) |
| 165 | | addcl 11237 |
. . . . . . . . 9
⊢ (((1 / 4)
∈ ℂ ∧ (𝑋
− (1 / 2)) ∈ ℂ) → ((1 / 4) + (𝑋 − (1 / 2))) ∈
ℂ) |
| 166 | 48, 71, 165 | sylancr 587 |
. . . . . . . 8
⊢ (𝑋 ∈ ℂ → ((1 / 4)
+ (𝑋 − (1 / 2)))
∈ ℂ) |
| 167 | 166, 131,
133 | addsub12d 11643 |
. . . . . . 7
⊢ (𝑋 ∈ ℂ → (((1 / 4)
+ (𝑋 − (1 / 2))) +
(((3 / 2) · (𝑋↑2)) − ((3 / 2) · (𝑋 − (1 / 6))))) = (((3 / 2)
· (𝑋↑2)) + (((1
/ 4) + (𝑋 − (1 / 2)))
− ((3 / 2) · (𝑋 − (1 / 6)))))) |
| 168 | 164, 167 | eqtrd 2777 |
. . . . . 6
⊢ (𝑋 ∈ ℂ →
(Σ𝑘 ∈
(0...1)((3C𝑘) ·
((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) + (((3 / 2) ·
(𝑋↑2)) − ((3 /
2) · (𝑋 − (1 /
6))))) = (((3 / 2) · (𝑋↑2)) + (((1 / 4) + (𝑋 − (1 / 2))) − ((3 / 2) ·
(𝑋 − (1 /
6)))))) |
| 169 | 133, 166 | negsubdi2d 11636 |
. . . . . . . 8
⊢ (𝑋 ∈ ℂ → -(((3 /
2) · (𝑋 − (1 /
6))) − ((1 / 4) + (𝑋
− (1 / 2)))) = (((1 / 4) + (𝑋 − (1 / 2))) − ((3 / 2) ·
(𝑋 − (1 /
6))))) |
| 170 | | subdi 11696 |
. . . . . . . . . . . 12
⊢ (((3 / 2)
∈ ℂ ∧ 𝑋
∈ ℂ ∧ (1 / 6) ∈ ℂ) → ((3 / 2) · (𝑋 − (1 / 6))) = (((3 / 2)
· 𝑋) − ((3 /
2) · (1 / 6)))) |
| 171 | 108, 118,
170 | mp3an13 1454 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → ((3 / 2)
· (𝑋 − (1 /
6))) = (((3 / 2) · 𝑋) − ((3 / 2) · (1 /
6)))) |
| 172 | | addsub12 11521 |
. . . . . . . . . . . 12
⊢ (((1 / 4)
∈ ℂ ∧ 𝑋
∈ ℂ ∧ (1 / 2) ∈ ℂ) → ((1 / 4) + (𝑋 − (1 / 2))) = (𝑋 + ((1 / 4) − (1 /
2)))) |
| 173 | 48, 69, 172 | mp3an13 1454 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → ((1 / 4)
+ (𝑋 − (1 / 2))) =
(𝑋 + ((1 / 4) − (1 /
2)))) |
| 174 | 171, 173 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ → (((3 / 2)
· (𝑋 − (1 /
6))) − ((1 / 4) + (𝑋
− (1 / 2)))) = ((((3 / 2) · 𝑋) − ((3 / 2) · (1 / 6)))
− (𝑋 + ((1 / 4)
− (1 / 2))))) |
| 175 | | mulcl 11239 |
. . . . . . . . . . . . 13
⊢ (((3 / 2)
∈ ℂ ∧ 𝑋
∈ ℂ) → ((3 / 2) · 𝑋) ∈ ℂ) |
| 176 | 108, 175 | mpan 690 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → ((3 / 2)
· 𝑋) ∈
ℂ) |
| 177 | 108, 118 | mulcli 11268 |
. . . . . . . . . . . 12
⊢ ((3 / 2)
· (1 / 6)) ∈ ℂ |
| 178 | | negsub 11557 |
. . . . . . . . . . . 12
⊢ ((((3 /
2) · 𝑋) ∈
ℂ ∧ ((3 / 2) · (1 / 6)) ∈ ℂ) → (((3 / 2)
· 𝑋) + -((3 / 2)
· (1 / 6))) = (((3 / 2) · 𝑋) − ((3 / 2) · (1 /
6)))) |
| 179 | 176, 177,
178 | sylancl 586 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → (((3 / 2)
· 𝑋) + -((3 / 2)
· (1 / 6))) = (((3 / 2) · 𝑋) − ((3 / 2) · (1 /
6)))) |
| 180 | 179 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ → ((((3 /
2) · 𝑋) + -((3 / 2)
· (1 / 6))) − (𝑋 + ((1 / 4) − (1 / 2)))) = ((((3 / 2)
· 𝑋) − ((3 /
2) · (1 / 6))) − (𝑋 + ((1 / 4) − (1 /
2))))) |
| 181 | 69, 48 | negsubdi2i 11595 |
. . . . . . . . . . . . . 14
⊢ -((1 / 2)
− (1 / 4)) = ((1 / 4) − (1 / 2)) |
| 182 | 85, 35, 85 | mul12i 11456 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2
· (3 · 2)) = (3 · (2 · 2)) |
| 183 | | 3t2e6 12432 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (3
· 2) = 6 |
| 184 | 183 | oveq2i 7442 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2
· (3 · 2)) = (2 · 6) |
| 185 | | 2t2e4 12430 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (2
· 2) = 4 |
| 186 | 185 | oveq2i 7442 |
. . . . . . . . . . . . . . . . . . 19
⊢ (3
· (2 · 2)) = (3 · 4) |
| 187 | 182, 184,
186 | 3eqtr3i 2773 |
. . . . . . . . . . . . . . . . . 18
⊢ (2
· 6) = (3 · 4) |
| 188 | 187 | oveq2i 7442 |
. . . . . . . . . . . . . . . . 17
⊢ ((3
· 1) / (2 · 6)) = ((3 · 1) / (3 ·
4)) |
| 189 | 46, 47 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . 18
⊢ (4 ∈
ℂ ∧ 4 ≠ 0) |
| 190 | 35, 72 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . 18
⊢ (3 ∈
ℂ ∧ 3 ≠ 0) |
| 191 | | divcan5 11969 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1
∈ ℂ ∧ (4 ∈ ℂ ∧ 4 ≠ 0) ∧ (3 ∈ ℂ
∧ 3 ≠ 0)) → ((3 · 1) / (3 · 4)) = (1 /
4)) |
| 192 | 60, 189, 190, 191 | mp3an 1463 |
. . . . . . . . . . . . . . . . 17
⊢ ((3
· 1) / (3 · 4)) = (1 / 4) |
| 193 | 188, 192 | eqtri 2765 |
. . . . . . . . . . . . . . . 16
⊢ ((3
· 1) / (2 · 6)) = (1 / 4) |
| 194 | 35, 85, 60, 114, 86, 117 | divmuldivi 12027 |
. . . . . . . . . . . . . . . 16
⊢ ((3 / 2)
· (1 / 6)) = ((3 · 1) / (2 · 6)) |
| 195 | | 2t1e2 12429 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (2
· 1) = 2 |
| 196 | 195, 5 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2
· 1) = (1 + 1) |
| 197 | 196, 185 | oveq12i 7443 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
· 1) / (2 · 2)) = ((1 + 1) / 4) |
| 198 | | divcan5 11969 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1
∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (2 ∈ ℂ
∧ 2 ≠ 0)) → ((2 · 1) / (2 · 2)) = (1 /
2)) |
| 199 | 60, 104, 104, 198 | mp3an 1463 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
· 1) / (2 · 2)) = (1 / 2) |
| 200 | 60, 60, 46, 47 | divdiri 12024 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1 + 1)
/ 4) = ((1 / 4) + (1 / 4)) |
| 201 | 197, 199,
200 | 3eqtr3ri 2774 |
. . . . . . . . . . . . . . . . 17
⊢ ((1 / 4)
+ (1 / 4)) = (1 / 2) |
| 202 | 69, 48, 48, 201 | subaddrii 11598 |
. . . . . . . . . . . . . . . 16
⊢ ((1 / 2)
− (1 / 4)) = (1 / 4) |
| 203 | 193, 194,
202 | 3eqtr4ri 2776 |
. . . . . . . . . . . . . . 15
⊢ ((1 / 2)
− (1 / 4)) = ((3 / 2) · (1 / 6)) |
| 204 | 203 | negeqi 11501 |
. . . . . . . . . . . . . 14
⊢ -((1 / 2)
− (1 / 4)) = -((3 / 2) · (1 / 6)) |
| 205 | 181, 204 | eqtr3i 2767 |
. . . . . . . . . . . . 13
⊢ ((1 / 4)
− (1 / 2)) = -((3 / 2) · (1 / 6)) |
| 206 | 48, 69 | subcli 11585 |
. . . . . . . . . . . . . 14
⊢ ((1 / 4)
− (1 / 2)) ∈ ℂ |
| 207 | 177 | negcli 11577 |
. . . . . . . . . . . . . 14
⊢ -((3 / 2)
· (1 / 6)) ∈ ℂ |
| 208 | 206, 207 | subeq0i 11589 |
. . . . . . . . . . . . 13
⊢ ((((1 /
4) − (1 / 2)) − -((3 / 2) · (1 / 6))) = 0 ↔ ((1 / 4)
− (1 / 2)) = -((3 / 2) · (1 / 6))) |
| 209 | 205, 208 | mpbir 231 |
. . . . . . . . . . . 12
⊢ (((1 / 4)
− (1 / 2)) − -((3 / 2) · (1 / 6))) = 0 |
| 210 | 209 | oveq2i 7442 |
. . . . . . . . . . 11
⊢ ((((3 /
2) · 𝑋) −
𝑋) − (((1 / 4)
− (1 / 2)) − -((3 / 2) · (1 / 6)))) = ((((3 / 2) ·
𝑋) − 𝑋) − 0) |
| 211 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → 𝑋 ∈
ℂ) |
| 212 | 206 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → ((1 / 4)
− (1 / 2)) ∈ ℂ) |
| 213 | 207 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → -((3 / 2)
· (1 / 6)) ∈ ℂ) |
| 214 | 176, 211,
212, 213 | subadd4d 11668 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → ((((3 /
2) · 𝑋) −
𝑋) − (((1 / 4)
− (1 / 2)) − -((3 / 2) · (1 / 6)))) = ((((3 / 2) ·
𝑋) + -((3 / 2) · (1
/ 6))) − (𝑋 + ((1 /
4) − (1 / 2))))) |
| 215 | | subdir 11697 |
. . . . . . . . . . . . . . 15
⊢ (((3 / 2)
∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑋 ∈ ℂ) → (((3 / 2) − 1)
· 𝑋) = (((3 / 2)
· 𝑋) − (1
· 𝑋))) |
| 216 | 108, 60, 215 | mp3an12 1453 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ ℂ → (((3 / 2)
− 1) · 𝑋) =
(((3 / 2) · 𝑋)
− (1 · 𝑋))) |
| 217 | | divsubdir 11961 |
. . . . . . . . . . . . . . . . . 18
⊢ ((3
∈ ℂ ∧ 2 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0))
→ ((3 − 2) / 2) = ((3 / 2) − (2 / 2))) |
| 218 | 35, 85, 104, 217 | mp3an 1463 |
. . . . . . . . . . . . . . . . 17
⊢ ((3
− 2) / 2) = ((3 / 2) − (2 / 2)) |
| 219 | 95 | oveq1i 7441 |
. . . . . . . . . . . . . . . . 17
⊢ ((3
− 2) / 2) = (1 / 2) |
| 220 | | 2div2e1 12407 |
. . . . . . . . . . . . . . . . . 18
⊢ (2 / 2) =
1 |
| 221 | 220 | oveq2i 7442 |
. . . . . . . . . . . . . . . . 17
⊢ ((3 / 2)
− (2 / 2)) = ((3 / 2) − 1) |
| 222 | 218, 219,
221 | 3eqtr3ri 2774 |
. . . . . . . . . . . . . . . 16
⊢ ((3 / 2)
− 1) = (1 / 2) |
| 223 | 222 | oveq1i 7441 |
. . . . . . . . . . . . . . 15
⊢ (((3 / 2)
− 1) · 𝑋) =
((1 / 2) · 𝑋) |
| 224 | 223 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ ℂ → (((3 / 2)
− 1) · 𝑋) =
((1 / 2) · 𝑋)) |
| 225 | | mullid 11260 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 ∈ ℂ → (1
· 𝑋) = 𝑋) |
| 226 | 225 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ ℂ → (((3 / 2)
· 𝑋) − (1
· 𝑋)) = (((3 / 2)
· 𝑋) − 𝑋)) |
| 227 | 216, 224,
226 | 3eqtr3rd 2786 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → (((3 / 2)
· 𝑋) − 𝑋) = ((1 / 2) · 𝑋)) |
| 228 | 227 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → ((((3 /
2) · 𝑋) −
𝑋) − 0) = (((1 / 2)
· 𝑋) −
0)) |
| 229 | | mulcl 11239 |
. . . . . . . . . . . . . 14
⊢ (((1 / 2)
∈ ℂ ∧ 𝑋
∈ ℂ) → ((1 / 2) · 𝑋) ∈ ℂ) |
| 230 | 69, 229 | mpan 690 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → ((1 / 2)
· 𝑋) ∈
ℂ) |
| 231 | 230 | subid1d 11609 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → (((1 / 2)
· 𝑋) − 0) =
((1 / 2) · 𝑋)) |
| 232 | 228, 231 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → ((((3 /
2) · 𝑋) −
𝑋) − 0) = ((1 / 2)
· 𝑋)) |
| 233 | 210, 214,
232 | 3eqtr3a 2801 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ → ((((3 /
2) · 𝑋) + -((3 / 2)
· (1 / 6))) − (𝑋 + ((1 / 4) − (1 / 2)))) = ((1 / 2)
· 𝑋)) |
| 234 | 174, 180,
233 | 3eqtr2d 2783 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℂ → (((3 / 2)
· (𝑋 − (1 /
6))) − ((1 / 4) + (𝑋
− (1 / 2)))) = ((1 / 2) · 𝑋)) |
| 235 | 234 | negeqd 11502 |
. . . . . . . 8
⊢ (𝑋 ∈ ℂ → -(((3 /
2) · (𝑋 − (1 /
6))) − ((1 / 4) + (𝑋
− (1 / 2)))) = -((1 / 2) · 𝑋)) |
| 236 | 169, 235 | eqtr3d 2779 |
. . . . . . 7
⊢ (𝑋 ∈ ℂ → (((1 / 4)
+ (𝑋 − (1 / 2)))
− ((3 / 2) · (𝑋 − (1 / 6)))) = -((1 / 2) ·
𝑋)) |
| 237 | 236 | oveq2d 7447 |
. . . . . 6
⊢ (𝑋 ∈ ℂ → (((3 / 2)
· (𝑋↑2)) + (((1
/ 4) + (𝑋 − (1 / 2)))
− ((3 / 2) · (𝑋 − (1 / 6))))) = (((3 / 2) ·
(𝑋↑2)) + -((1 / 2)
· 𝑋))) |
| 238 | 131, 230 | negsubd 11626 |
. . . . . 6
⊢ (𝑋 ∈ ℂ → (((3 / 2)
· (𝑋↑2)) + -((1
/ 2) · 𝑋)) = (((3 /
2) · (𝑋↑2))
− ((1 / 2) · 𝑋))) |
| 239 | 168, 237,
238 | 3eqtrd 2781 |
. . . . 5
⊢ (𝑋 ∈ ℂ →
(Σ𝑘 ∈
(0...1)((3C𝑘) ·
((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) + (((3 / 2) ·
(𝑋↑2)) − ((3 /
2) · (𝑋 − (1 /
6))))) = (((3 / 2) · (𝑋↑2)) − ((1 / 2) · 𝑋))) |
| 240 | 141, 142,
239 | 3eqtrd 2781 |
. . . 4
⊢ (𝑋 ∈ ℂ →
Σ𝑘 ∈ (0...(1 +
1))((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (((3 / 2) · (𝑋↑2)) − ((1 / 2)
· 𝑋))) |
| 241 | 8, 240 | eqtrid 2789 |
. . 3
⊢ (𝑋 ∈ ℂ →
Σ𝑘 ∈ (0...(3
− 1))((3C𝑘) ·
((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (((3 / 2) ·
(𝑋↑2)) − ((1 /
2) · 𝑋))) |
| 242 | 241 | oveq2d 7447 |
. 2
⊢ (𝑋 ∈ ℂ → ((𝑋↑3) − Σ𝑘 ∈ (0...(3 −
1))((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1)))) = ((𝑋↑3) − (((3 / 2) · (𝑋↑2)) − ((1 / 2)
· 𝑋)))) |
| 243 | | expcl 14120 |
. . . 4
⊢ ((𝑋 ∈ ℂ ∧ 3 ∈
ℕ0) → (𝑋↑3) ∈ ℂ) |
| 244 | 1, 243 | mpan2 691 |
. . 3
⊢ (𝑋 ∈ ℂ → (𝑋↑3) ∈
ℂ) |
| 245 | 244, 131,
230 | subsubd 11648 |
. 2
⊢ (𝑋 ∈ ℂ → ((𝑋↑3) − (((3 / 2)
· (𝑋↑2))
− ((1 / 2) · 𝑋))) = (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) ·
𝑋))) |
| 246 | 3, 242, 245 | 3eqtrd 2781 |
1
⊢ (𝑋 ∈ ℂ → (3
BernPoly 𝑋) = (((𝑋↑3) − ((3 / 2)
· (𝑋↑2))) + ((1
/ 2) · 𝑋))) |