Step | Hyp | Ref
| Expression |
1 | | 3nn0 11187 |
. . 3
⊢ 3 ∈
ℕ0 |
2 | | bpolyval 14619 |
. . 3
⊢ ((3
∈ ℕ0 ∧ 𝑋 ∈ ℂ) → (3 BernPoly 𝑋) = ((𝑋↑3) − Σ𝑘 ∈ (0...(3 − 1))((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))))) |
3 | 1, 2 | mpan 702 |
. 2
⊢ (𝑋 ∈ ℂ → (3
BernPoly 𝑋) = ((𝑋↑3) − Σ𝑘 ∈ (0...(3 −
1))((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))))) |
4 | | 3m1e2 11014 |
. . . . . . 7
⊢ (3
− 1) = 2 |
5 | | df-2 10956 |
. . . . . . 7
⊢ 2 = (1 +
1) |
6 | 4, 5 | eqtri 2632 |
. . . . . 6
⊢ (3
− 1) = (1 + 1) |
7 | 6 | oveq2i 6560 |
. . . . 5
⊢ (0...(3
− 1)) = (0...(1 + 1)) |
8 | 7 | sumeq1i 14276 |
. . . 4
⊢
Σ𝑘 ∈
(0...(3 − 1))((3C𝑘)
· ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = Σ𝑘 ∈ (0...(1 + 1))((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) |
9 | | 1eluzge0 11608 |
. . . . . . 7
⊢ 1 ∈
(ℤ≥‘0) |
10 | 9 | a1i 11 |
. . . . . 6
⊢ (𝑋 ∈ ℂ → 1 ∈
(ℤ≥‘0)) |
11 | | 0z 11265 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℤ |
12 | | fzpr 12266 |
. . . . . . . . . . . . 13
⊢ (0 ∈
ℤ → (0...(0 + 1)) = {0, (0 + 1)}) |
13 | 11, 12 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (0...(0 +
1)) = {0, (0 + 1)} |
14 | | 0p1e1 11009 |
. . . . . . . . . . . . 13
⊢ (0 + 1) =
1 |
15 | 14 | oveq2i 6560 |
. . . . . . . . . . . 12
⊢ (0...(0 +
1)) = (0...1) |
16 | 14 | preq2i 4216 |
. . . . . . . . . . . 12
⊢ {0, (0 +
1)} = {0, 1} |
17 | 13, 15, 16 | 3eqtr3ri 2641 |
. . . . . . . . . . 11
⊢ {0, 1} =
(0...1) |
18 | 5 | sneqi 4136 |
. . . . . . . . . . 11
⊢ {2} = {(1
+ 1)} |
19 | 17, 18 | uneq12i 3727 |
. . . . . . . . . 10
⊢ ({0, 1}
∪ {2}) = ((0...1) ∪ {(1 + 1)}) |
20 | | df-tp 4130 |
. . . . . . . . . 10
⊢ {0, 1, 2}
= ({0, 1} ∪ {2}) |
21 | | fzsuc 12258 |
. . . . . . . . . . 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 2643 |
. . . . . . . . 9
⊢ (0...(1 +
1)) = {0, 1, 2} |
24 | 23 | eleq2i 2680 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...(1 + 1)) ↔
𝑘 ∈ {0, 1,
2}) |
25 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑘 ∈ V |
26 | 25 | eltp 4177 |
. . . . . . . 8
⊢ (𝑘 ∈ {0, 1, 2} ↔ (𝑘 = 0 ∨ 𝑘 = 1 ∨ 𝑘 = 2)) |
27 | 24, 26 | bitri 263 |
. . . . . . 7
⊢ (𝑘 ∈ (0...(1 + 1)) ↔
(𝑘 = 0 ∨ 𝑘 = 1 ∨ 𝑘 = 2)) |
28 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑘 = 0 → (3C𝑘) = (3C0)) |
29 | | bcn0 12959 |
. . . . . . . . . . . . 13
⊢ (3 ∈
ℕ0 → (3C0) = 1) |
30 | 1, 29 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (3C0) =
1 |
31 | 28, 30 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ (𝑘 = 0 → (3C𝑘) = 1) |
32 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑘 = 0 → (𝑘 BernPoly 𝑋) = (0 BernPoly 𝑋)) |
33 | | oveq2 6557 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 0 → (3 − 𝑘) = (3 −
0)) |
34 | 33 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 0 → ((3 − 𝑘) + 1) = ((3 − 0) +
1)) |
35 | | 3cn 10972 |
. . . . . . . . . . . . . . . 16
⊢ 3 ∈
ℂ |
36 | 35 | subid1i 10232 |
. . . . . . . . . . . . . . 15
⊢ (3
− 0) = 3 |
37 | 36 | oveq1i 6559 |
. . . . . . . . . . . . . 14
⊢ ((3
− 0) + 1) = (3 + 1) |
38 | | df-4 10958 |
. . . . . . . . . . . . . 14
⊢ 4 = (3 +
1) |
39 | 37, 38 | eqtr4i 2635 |
. . . . . . . . . . . . 13
⊢ ((3
− 0) + 1) = 4 |
40 | 34, 39 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ (𝑘 = 0 → ((3 − 𝑘) + 1) = 4) |
41 | 32, 40 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (𝑘 = 0 → ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1)) = ((0 BernPoly 𝑋) / 4)) |
42 | 31, 41 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑘 = 0 → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (1 · ((0 BernPoly 𝑋) / 4))) |
43 | | bpoly0 14620 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → (0
BernPoly 𝑋) =
1) |
44 | 43 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → ((0
BernPoly 𝑋) / 4) = (1 /
4)) |
45 | 44 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → (1
· ((0 BernPoly 𝑋) /
4)) = (1 · (1 / 4))) |
46 | | 4cn 10975 |
. . . . . . . . . . . . 13
⊢ 4 ∈
ℂ |
47 | | 4ne0 10994 |
. . . . . . . . . . . . 13
⊢ 4 ≠
0 |
48 | 46, 47 | reccli 10634 |
. . . . . . . . . . . 12
⊢ (1 / 4)
∈ ℂ |
49 | 48 | mulid2i 9922 |
. . . . . . . . . . 11
⊢ (1
· (1 / 4)) = (1 / 4) |
50 | 45, 49 | syl6eq 2660 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ → (1
· ((0 BernPoly 𝑋) /
4)) = (1 / 4)) |
51 | 42, 50 | sylan9eqr 2666 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 = 0) → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (1 / 4)) |
52 | 51, 48 | syl6eqel 2696 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 = 0) → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) ∈ ℂ) |
53 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑘 = 1 → (3C𝑘) = (3C1)) |
54 | | bcn1 12962 |
. . . . . . . . . . . . 13
⊢ (3 ∈
ℕ0 → (3C1) = 3) |
55 | 1, 54 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (3C1) =
3 |
56 | 53, 55 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ (𝑘 = 1 → (3C𝑘) = 3) |
57 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑘 = 1 → (𝑘 BernPoly 𝑋) = (1 BernPoly 𝑋)) |
58 | | oveq2 6557 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 1 → (3 − 𝑘) = (3 −
1)) |
59 | 58 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 1 → ((3 − 𝑘) + 1) = ((3 − 1) +
1)) |
60 | | ax-1cn 9873 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℂ |
61 | | npcan 10169 |
. . . . . . . . . . . . . 14
⊢ ((3
∈ ℂ ∧ 1 ∈ ℂ) → ((3 − 1) + 1) =
3) |
62 | 35, 60, 61 | mp2an 704 |
. . . . . . . . . . . . 13
⊢ ((3
− 1) + 1) = 3 |
63 | 59, 62 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ (𝑘 = 1 → ((3 − 𝑘) + 1) = 3) |
64 | 57, 63 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (𝑘 = 1 → ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1)) = ((1 BernPoly 𝑋) / 3)) |
65 | 56, 64 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑘 = 1 → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (3 · ((1 BernPoly 𝑋) / 3))) |
66 | | bpoly1 14621 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → (1
BernPoly 𝑋) = (𝑋 − (1 /
2))) |
67 | 66 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → ((1
BernPoly 𝑋) / 3) = ((𝑋 − (1 / 2)) /
3)) |
68 | 67 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → (3
· ((1 BernPoly 𝑋) /
3)) = (3 · ((𝑋
− (1 / 2)) / 3))) |
69 | | halfcn 11124 |
. . . . . . . . . . . . 13
⊢ (1 / 2)
∈ ℂ |
70 | | subcl 10159 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ ℂ ∧ (1 / 2)
∈ ℂ) → (𝑋
− (1 / 2)) ∈ ℂ) |
71 | 69, 70 | mpan2 703 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → (𝑋 − (1 / 2)) ∈
ℂ) |
72 | | 3ne0 10992 |
. . . . . . . . . . . . 13
⊢ 3 ≠
0 |
73 | | divcan2 10572 |
. . . . . . . . . . . . 13
⊢ (((𝑋 − (1 / 2)) ∈ ℂ
∧ 3 ∈ ℂ ∧ 3 ≠ 0) → (3 · ((𝑋 − (1 / 2)) / 3)) = (𝑋 − (1 / 2))) |
74 | 35, 72, 73 | mp3an23 1408 |
. . . . . . . . . . . 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 2644 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ → (3
· ((1 BernPoly 𝑋) /
3)) = (𝑋 − (1 /
2))) |
77 | 65, 76 | sylan9eqr 2666 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 = 1) → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (𝑋 − (1 / 2))) |
78 | 71 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 = 1) → (𝑋 − (1 / 2)) ∈
ℂ) |
79 | 77, 78 | eqeltrd 2688 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 = 1) → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) ∈ ℂ) |
80 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑘 = 2 → (3C𝑘) = (3C2)) |
81 | | bcn2 12968 |
. . . . . . . . . . . . . 14
⊢ (3 ∈
ℕ0 → (3C2) = ((3 · (3 − 1)) /
2)) |
82 | 1, 81 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (3C2) =
((3 · (3 − 1)) / 2) |
83 | 4 | oveq2i 6560 |
. . . . . . . . . . . . . . 15
⊢ (3
· (3 − 1)) = (3 · 2) |
84 | 83 | oveq1i 6559 |
. . . . . . . . . . . . . 14
⊢ ((3
· (3 − 1)) / 2) = ((3 · 2) / 2) |
85 | | 2cn 10968 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℂ |
86 | | 2ne0 10990 |
. . . . . . . . . . . . . . 15
⊢ 2 ≠
0 |
87 | 35, 85, 86 | divcan4i 10651 |
. . . . . . . . . . . . . 14
⊢ ((3
· 2) / 2) = 3 |
88 | 84, 87 | eqtri 2632 |
. . . . . . . . . . . . 13
⊢ ((3
· (3 − 1)) / 2) = 3 |
89 | 82, 88 | eqtri 2632 |
. . . . . . . . . . . 12
⊢ (3C2) =
3 |
90 | 80, 89 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ (𝑘 = 2 → (3C𝑘) = 3) |
91 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑘 = 2 → (𝑘 BernPoly 𝑋) = (2 BernPoly 𝑋)) |
92 | | oveq2 6557 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 2 → (3 − 𝑘) = (3 −
2)) |
93 | 92 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 2 → ((3 − 𝑘) + 1) = ((3 − 2) +
1)) |
94 | | 2p1e3 11028 |
. . . . . . . . . . . . . . . 16
⊢ (2 + 1) =
3 |
95 | 35, 85, 60, 94 | subaddrii 10249 |
. . . . . . . . . . . . . . 15
⊢ (3
− 2) = 1 |
96 | 95 | oveq1i 6559 |
. . . . . . . . . . . . . 14
⊢ ((3
− 2) + 1) = (1 + 1) |
97 | 96, 5 | eqtr4i 2635 |
. . . . . . . . . . . . 13
⊢ ((3
− 2) + 1) = 2 |
98 | 93, 97 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ (𝑘 = 2 → ((3 − 𝑘) + 1) = 2) |
99 | 91, 98 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (𝑘 = 2 → ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1)) = ((2 BernPoly 𝑋) / 2)) |
100 | 90, 99 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑘 = 2 → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (3 · ((2 BernPoly 𝑋) / 2))) |
101 | | 2nn0 11186 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ0 |
102 | | bpolycl 14622 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℕ0 ∧ 𝑋 ∈ ℂ) → (2 BernPoly 𝑋) ∈
ℂ) |
103 | 101, 102 | mpan 702 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → (2
BernPoly 𝑋) ∈
ℂ) |
104 | | 2cnne0 11119 |
. . . . . . . . . . . . 13
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
105 | | div12 10586 |
. . . . . . . . . . . . 13
⊢ ((3
∈ ℂ ∧ (2 BernPoly 𝑋) ∈ ℂ ∧ (2 ∈ ℂ
∧ 2 ≠ 0)) → (3 · ((2 BernPoly 𝑋) / 2)) = ((2 BernPoly 𝑋) · (3 / 2))) |
106 | 35, 104, 105 | mp3an13 1407 |
. . . . . . . . . . . 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 10646 |
. . . . . . . . . . . 12
⊢ (3 / 2)
∈ ℂ |
109 | | mulcom 9901 |
. . . . . . . . . . . 12
⊢ (((2
BernPoly 𝑋) ∈ ℂ
∧ (3 / 2) ∈ ℂ) → ((2 BernPoly 𝑋) · (3 / 2)) = ((3 / 2) · (2
BernPoly 𝑋))) |
110 | 103, 108,
109 | sylancl 693 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → ((2
BernPoly 𝑋) · (3 /
2)) = ((3 / 2) · (2 BernPoly 𝑋))) |
111 | | bpoly2 14627 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → (2
BernPoly 𝑋) = (((𝑋↑2) − 𝑋) + (1 / 6))) |
112 | 111 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → ((3 / 2)
· (2 BernPoly 𝑋)) =
((3 / 2) · (((𝑋↑2) − 𝑋) + (1 / 6)))) |
113 | | sqcl 12787 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ ℂ → (𝑋↑2) ∈
ℂ) |
114 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ ℂ → 𝑋 ∈
ℂ) |
115 | | 6cn 10979 |
. . . . . . . . . . . . . . . 16
⊢ 6 ∈
ℂ |
116 | | 6re 10978 |
. . . . . . . . . . . . . . . . 17
⊢ 6 ∈
ℝ |
117 | | 6pos 10996 |
. . . . . . . . . . . . . . . . 17
⊢ 0 <
6 |
118 | 116, 117 | gt0ne0ii 10443 |
. . . . . . . . . . . . . . . 16
⊢ 6 ≠
0 |
119 | 115, 118 | reccli 10634 |
. . . . . . . . . . . . . . 15
⊢ (1 / 6)
∈ ℂ |
120 | | subsub 10190 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋↑2) ∈ ℂ ∧
𝑋 ∈ ℂ ∧ (1 /
6) ∈ ℂ) → ((𝑋↑2) − (𝑋 − (1 / 6))) = (((𝑋↑2) − 𝑋) + (1 / 6))) |
121 | 119, 120 | mp3an3 1405 |
. . . . . . . . . . . . . 14
⊢ (((𝑋↑2) ∈ ℂ ∧
𝑋 ∈ ℂ) →
((𝑋↑2) − (𝑋 − (1 / 6))) = (((𝑋↑2) − 𝑋) + (1 / 6))) |
122 | 113, 114,
121 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → ((𝑋↑2) − (𝑋 − (1 / 6))) = (((𝑋↑2) − 𝑋) + (1 / 6))) |
123 | 122 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → ((3 / 2)
· ((𝑋↑2)
− (𝑋 − (1 /
6)))) = ((3 / 2) · (((𝑋↑2) − 𝑋) + (1 / 6)))) |
124 | | subcl 10159 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ ℂ ∧ (1 / 6)
∈ ℂ) → (𝑋
− (1 / 6)) ∈ ℂ) |
125 | 119, 124 | mpan2 703 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → (𝑋 − (1 / 6)) ∈
ℂ) |
126 | | subdi 10342 |
. . . . . . . . . . . . . 14
⊢ (((3 / 2)
∈ ℂ ∧ (𝑋↑2) ∈ ℂ ∧ (𝑋 − (1 / 6)) ∈
ℂ) → ((3 / 2) · ((𝑋↑2) − (𝑋 − (1 / 6)))) = (((3 / 2) ·
(𝑋↑2)) − ((3 /
2) · (𝑋 − (1 /
6))))) |
127 | 108, 126 | mp3an1 1403 |
. . . . . . . . . . . . 13
⊢ (((𝑋↑2) ∈ ℂ ∧
(𝑋 − (1 / 6)) ∈
ℂ) → ((3 / 2) · ((𝑋↑2) − (𝑋 − (1 / 6)))) = (((3 / 2) ·
(𝑋↑2)) − ((3 /
2) · (𝑋 − (1 /
6))))) |
128 | 113, 125,
127 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → ((3 / 2)
· ((𝑋↑2)
− (𝑋 − (1 /
6)))) = (((3 / 2) · (𝑋↑2)) − ((3 / 2) · (𝑋 − (1 /
6))))) |
129 | 112, 123,
128 | 3eqtr2d 2650 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → ((3 / 2)
· (2 BernPoly 𝑋)) =
(((3 / 2) · (𝑋↑2)) − ((3 / 2) · (𝑋 − (1 /
6))))) |
130 | 107, 110,
129 | 3eqtrd 2648 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ → (3
· ((2 BernPoly 𝑋) /
2)) = (((3 / 2) · (𝑋↑2)) − ((3 / 2) · (𝑋 − (1 /
6))))) |
131 | 100, 130 | sylan9eqr 2666 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 = 2) → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (((3 / 2) · (𝑋↑2)) − ((3 / 2)
· (𝑋 − (1 /
6))))) |
132 | | mulcl 9899 |
. . . . . . . . . . . 12
⊢ (((3 / 2)
∈ ℂ ∧ (𝑋↑2) ∈ ℂ) → ((3 / 2)
· (𝑋↑2)) ∈
ℂ) |
133 | 108, 113,
132 | sylancr 694 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → ((3 / 2)
· (𝑋↑2)) ∈
ℂ) |
134 | | mulcl 9899 |
. . . . . . . . . . . 12
⊢ (((3 / 2)
∈ ℂ ∧ (𝑋
− (1 / 6)) ∈ ℂ) → ((3 / 2) · (𝑋 − (1 / 6))) ∈
ℂ) |
135 | 108, 125,
134 | sylancr 694 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → ((3 / 2)
· (𝑋 − (1 /
6))) ∈ ℂ) |
136 | 133, 135 | subcld 10271 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ → (((3 / 2)
· (𝑋↑2))
− ((3 / 2) · (𝑋 − (1 / 6)))) ∈
ℂ) |
137 | 136 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 = 2) → (((3 / 2) ·
(𝑋↑2)) − ((3 /
2) · (𝑋 − (1 /
6)))) ∈ ℂ) |
138 | 131, 137 | eqeltrd 2688 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 = 2) → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) ∈ ℂ) |
139 | 52, 79, 138 | 3jaodan 1386 |
. . . . . . 7
⊢ ((𝑋 ∈ ℂ ∧ (𝑘 = 0 ∨ 𝑘 = 1 ∨ 𝑘 = 2)) → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) ∈ ℂ) |
140 | 27, 139 | sylan2b 491 |
. . . . . 6
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(1 + 1))) →
((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) ∈ ℂ) |
141 | 5 | eqeq2i 2622 |
. . . . . . 7
⊢ (𝑘 = 2 ↔ 𝑘 = (1 + 1)) |
142 | 141, 100 | sylbir 224 |
. . . . . 6
⊢ (𝑘 = (1 + 1) → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (3 · ((2 BernPoly 𝑋) / 2))) |
143 | 10, 140, 142 | fsump1 14329 |
. . . . 5
⊢ (𝑋 ∈ ℂ →
Σ𝑘 ∈ (0...(1 +
1))((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (Σ𝑘 ∈ (0...1)((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) + (3 · ((2 BernPoly 𝑋) / 2)))) |
144 | 130 | oveq2d 6565 |
. . . . 5
⊢ (𝑋 ∈ ℂ →
(Σ𝑘 ∈
(0...1)((3C𝑘) ·
((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) + (3 · ((2
BernPoly 𝑋) / 2))) =
(Σ𝑘 ∈
(0...1)((3C𝑘) ·
((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) + (((3 / 2) ·
(𝑋↑2)) − ((3 /
2) · (𝑋 − (1 /
6)))))) |
145 | 15 | sumeq1i 14276 |
. . . . . . . . 9
⊢
Σ𝑘 ∈
(0...(0 + 1))((3C𝑘)
· ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = Σ𝑘 ∈ (0...1)((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) |
146 | | 0nn0 11184 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℕ0 |
147 | | nn0uz 11598 |
. . . . . . . . . . . . 13
⊢
ℕ0 = (ℤ≥‘0) |
148 | 146, 147 | eleqtri 2686 |
. . . . . . . . . . . 12
⊢ 0 ∈
(ℤ≥‘0) |
149 | 148 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → 0 ∈
(ℤ≥‘0)) |
150 | 13, 16 | eqtri 2632 |
. . . . . . . . . . . . . 14
⊢ (0...(0 +
1)) = {0, 1} |
151 | 150 | eleq2i 2680 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0...(0 + 1)) ↔
𝑘 ∈ {0,
1}) |
152 | 25 | elpr 4146 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ {0, 1} ↔ (𝑘 = 0 ∨ 𝑘 = 1)) |
153 | 151, 152 | bitri 263 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (0...(0 + 1)) ↔
(𝑘 = 0 ∨ 𝑘 = 1)) |
154 | 52, 79 | jaodan 822 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ ℂ ∧ (𝑘 = 0 ∨ 𝑘 = 1)) → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) ∈ ℂ) |
155 | 153, 154 | sylan2b 491 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(0 + 1))) →
((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) ∈ ℂ) |
156 | 14 | eqeq2i 2622 |
. . . . . . . . . . . 12
⊢ (𝑘 = (0 + 1) ↔ 𝑘 = 1) |
157 | 156, 65 | sylbi 206 |
. . . . . . . . . . 11
⊢ (𝑘 = (0 + 1) → ((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (3 · ((1 BernPoly 𝑋) / 3))) |
158 | 149, 155,
157 | fsump1 14329 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ →
Σ𝑘 ∈ (0...(0 +
1))((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (Σ𝑘 ∈ (0...0)((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) + (3 · ((1 BernPoly 𝑋) / 3)))) |
159 | 50, 48 | syl6eqel 2696 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → (1
· ((0 BernPoly 𝑋) /
4)) ∈ ℂ) |
160 | 42 | fsum1 14320 |
. . . . . . . . . . . . 13
⊢ ((0
∈ ℤ ∧ (1 · ((0 BernPoly 𝑋) / 4)) ∈ ℂ) → Σ𝑘 ∈ (0...0)((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (1 · ((0 BernPoly 𝑋) / 4))) |
161 | 11, 159, 160 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ →
Σ𝑘 ∈
(0...0)((3C𝑘) ·
((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (1 · ((0
BernPoly 𝑋) /
4))) |
162 | 161, 50 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ →
Σ𝑘 ∈
(0...0)((3C𝑘) ·
((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (1 /
4)) |
163 | 162, 76 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ →
(Σ𝑘 ∈
(0...0)((3C𝑘) ·
((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) + (3 · ((1
BernPoly 𝑋) / 3))) = ((1 /
4) + (𝑋 − (1 /
2)))) |
164 | 158, 163 | eqtrd 2644 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℂ →
Σ𝑘 ∈ (0...(0 +
1))((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = ((1 / 4) + (𝑋 − (1 / 2)))) |
165 | 145, 164 | syl5eqr 2658 |
. . . . . . . 8
⊢ (𝑋 ∈ ℂ →
Σ𝑘 ∈
(0...1)((3C𝑘) ·
((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = ((1 / 4) + (𝑋 − (1 /
2)))) |
166 | 165 | oveq1d 6564 |
. . . . . . 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)))))) |
167 | | addcl 9897 |
. . . . . . . . 9
⊢ (((1 / 4)
∈ ℂ ∧ (𝑋
− (1 / 2)) ∈ ℂ) → ((1 / 4) + (𝑋 − (1 / 2))) ∈
ℂ) |
168 | 48, 71, 167 | sylancr 694 |
. . . . . . . 8
⊢ (𝑋 ∈ ℂ → ((1 / 4)
+ (𝑋 − (1 / 2)))
∈ ℂ) |
169 | 168, 133,
135 | addsub12d 10294 |
. . . . . . 7
⊢ (𝑋 ∈ ℂ → (((1 / 4)
+ (𝑋 − (1 / 2))) +
(((3 / 2) · (𝑋↑2)) − ((3 / 2) · (𝑋 − (1 / 6))))) = (((3 / 2)
· (𝑋↑2)) + (((1
/ 4) + (𝑋 − (1 / 2)))
− ((3 / 2) · (𝑋 − (1 / 6)))))) |
170 | 166, 169 | eqtrd 2644 |
. . . . . 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)))))) |
171 | 135, 168 | negsubdi2d 10287 |
. . . . . . . 8
⊢ (𝑋 ∈ ℂ → -(((3 /
2) · (𝑋 − (1 /
6))) − ((1 / 4) + (𝑋
− (1 / 2)))) = (((1 / 4) + (𝑋 − (1 / 2))) − ((3 / 2) ·
(𝑋 − (1 /
6))))) |
172 | | subdi 10342 |
. . . . . . . . . . . 12
⊢ (((3 / 2)
∈ ℂ ∧ 𝑋
∈ ℂ ∧ (1 / 6) ∈ ℂ) → ((3 / 2) · (𝑋 − (1 / 6))) = (((3 / 2)
· 𝑋) − ((3 /
2) · (1 / 6)))) |
173 | 108, 119,
172 | mp3an13 1407 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → ((3 / 2)
· (𝑋 − (1 /
6))) = (((3 / 2) · 𝑋) − ((3 / 2) · (1 /
6)))) |
174 | | addsub12 10173 |
. . . . . . . . . . . 12
⊢ (((1 / 4)
∈ ℂ ∧ 𝑋
∈ ℂ ∧ (1 / 2) ∈ ℂ) → ((1 / 4) + (𝑋 − (1 / 2))) = (𝑋 + ((1 / 4) − (1 /
2)))) |
175 | 48, 69, 174 | mp3an13 1407 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → ((1 / 4)
+ (𝑋 − (1 / 2))) =
(𝑋 + ((1 / 4) − (1 /
2)))) |
176 | 173, 175 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ → (((3 / 2)
· (𝑋 − (1 /
6))) − ((1 / 4) + (𝑋
− (1 / 2)))) = ((((3 / 2) · 𝑋) − ((3 / 2) · (1 / 6)))
− (𝑋 + ((1 / 4)
− (1 / 2))))) |
177 | | mulcl 9899 |
. . . . . . . . . . . . 13
⊢ (((3 / 2)
∈ ℂ ∧ 𝑋
∈ ℂ) → ((3 / 2) · 𝑋) ∈ ℂ) |
178 | 108, 177 | mpan 702 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → ((3 / 2)
· 𝑋) ∈
ℂ) |
179 | 108, 119 | mulcli 9924 |
. . . . . . . . . . . 12
⊢ ((3 / 2)
· (1 / 6)) ∈ ℂ |
180 | | negsub 10208 |
. . . . . . . . . . . 12
⊢ ((((3 /
2) · 𝑋) ∈
ℂ ∧ ((3 / 2) · (1 / 6)) ∈ ℂ) → (((3 / 2)
· 𝑋) + -((3 / 2)
· (1 / 6))) = (((3 / 2) · 𝑋) − ((3 / 2) · (1 /
6)))) |
181 | 178, 179,
180 | sylancl 693 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → (((3 / 2)
· 𝑋) + -((3 / 2)
· (1 / 6))) = (((3 / 2) · 𝑋) − ((3 / 2) · (1 /
6)))) |
182 | 181 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ → ((((3 /
2) · 𝑋) + -((3 / 2)
· (1 / 6))) − (𝑋 + ((1 / 4) − (1 / 2)))) = ((((3 / 2)
· 𝑋) − ((3 /
2) · (1 / 6))) − (𝑋 + ((1 / 4) − (1 /
2))))) |
183 | 69, 48 | negsubdi2i 10246 |
. . . . . . . . . . . . . 14
⊢ -((1 / 2)
− (1 / 4)) = ((1 / 4) − (1 / 2)) |
184 | 85, 35, 85 | mul12i 10110 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2
· (3 · 2)) = (3 · (2 · 2)) |
185 | | 3t2e6 11056 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (3
· 2) = 6 |
186 | 185 | oveq2i 6560 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2
· (3 · 2)) = (2 · 6) |
187 | | 2t2e4 11054 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (2
· 2) = 4 |
188 | 187 | oveq2i 6560 |
. . . . . . . . . . . . . . . . . . 19
⊢ (3
· (2 · 2)) = (3 · 4) |
189 | 184, 186,
188 | 3eqtr3i 2640 |
. . . . . . . . . . . . . . . . . 18
⊢ (2
· 6) = (3 · 4) |
190 | 189 | oveq2i 6560 |
. . . . . . . . . . . . . . . . 17
⊢ ((3
· 1) / (2 · 6)) = ((3 · 1) / (3 ·
4)) |
191 | 46, 47 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . 18
⊢ (4 ∈
ℂ ∧ 4 ≠ 0) |
192 | 35, 72 | pm3.2i 470 |
. . . . . . . . . . . . . . . . . 18
⊢ (3 ∈
ℂ ∧ 3 ≠ 0) |
193 | | divcan5 10606 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1
∈ ℂ ∧ (4 ∈ ℂ ∧ 4 ≠ 0) ∧ (3 ∈ ℂ
∧ 3 ≠ 0)) → ((3 · 1) / (3 · 4)) = (1 /
4)) |
194 | 60, 191, 192, 193 | mp3an 1416 |
. . . . . . . . . . . . . . . . 17
⊢ ((3
· 1) / (3 · 4)) = (1 / 4) |
195 | 190, 194 | eqtri 2632 |
. . . . . . . . . . . . . . . 16
⊢ ((3
· 1) / (2 · 6)) = (1 / 4) |
196 | 35, 85, 60, 115, 86, 118 | divmuldivi 10664 |
. . . . . . . . . . . . . . . 16
⊢ ((3 / 2)
· (1 / 6)) = ((3 · 1) / (2 · 6)) |
197 | | 2t1e2 11053 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (2
· 1) = 2 |
198 | 197, 5 | eqtri 2632 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2
· 1) = (1 + 1) |
199 | 198, 187 | oveq12i 6561 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
· 1) / (2 · 2)) = ((1 + 1) / 4) |
200 | | divcan5 10606 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1
∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (2 ∈ ℂ
∧ 2 ≠ 0)) → ((2 · 1) / (2 · 2)) = (1 /
2)) |
201 | 60, 104, 104, 200 | mp3an 1416 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
· 1) / (2 · 2)) = (1 / 2) |
202 | 60, 60, 46, 47 | divdiri 10661 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1 + 1)
/ 4) = ((1 / 4) + (1 / 4)) |
203 | 199, 201,
202 | 3eqtr3ri 2641 |
. . . . . . . . . . . . . . . . 17
⊢ ((1 / 4)
+ (1 / 4)) = (1 / 2) |
204 | 69, 48, 48, 203 | subaddrii 10249 |
. . . . . . . . . . . . . . . 16
⊢ ((1 / 2)
− (1 / 4)) = (1 / 4) |
205 | 195, 196,
204 | 3eqtr4ri 2643 |
. . . . . . . . . . . . . . 15
⊢ ((1 / 2)
− (1 / 4)) = ((3 / 2) · (1 / 6)) |
206 | 205 | negeqi 10153 |
. . . . . . . . . . . . . 14
⊢ -((1 / 2)
− (1 / 4)) = -((3 / 2) · (1 / 6)) |
207 | 183, 206 | eqtr3i 2634 |
. . . . . . . . . . . . 13
⊢ ((1 / 4)
− (1 / 2)) = -((3 / 2) · (1 / 6)) |
208 | 48, 69 | subcli 10236 |
. . . . . . . . . . . . . 14
⊢ ((1 / 4)
− (1 / 2)) ∈ ℂ |
209 | 179 | negcli 10228 |
. . . . . . . . . . . . . 14
⊢ -((3 / 2)
· (1 / 6)) ∈ ℂ |
210 | 208, 209 | subeq0i 10240 |
. . . . . . . . . . . . 13
⊢ ((((1 /
4) − (1 / 2)) − -((3 / 2) · (1 / 6))) = 0 ↔ ((1 / 4)
− (1 / 2)) = -((3 / 2) · (1 / 6))) |
211 | 207, 210 | mpbir 220 |
. . . . . . . . . . . 12
⊢ (((1 / 4)
− (1 / 2)) − -((3 / 2) · (1 / 6))) = 0 |
212 | 211 | oveq2i 6560 |
. . . . . . . . . . 11
⊢ ((((3 /
2) · 𝑋) −
𝑋) − (((1 / 4)
− (1 / 2)) − -((3 / 2) · (1 / 6)))) = ((((3 / 2) ·
𝑋) − 𝑋) − 0) |
213 | 208 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → ((1 / 4)
− (1 / 2)) ∈ ℂ) |
214 | 209 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → -((3 / 2)
· (1 / 6)) ∈ ℂ) |
215 | 178, 114,
213, 214 | subadd4d 10319 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → ((((3 /
2) · 𝑋) −
𝑋) − (((1 / 4)
− (1 / 2)) − -((3 / 2) · (1 / 6)))) = ((((3 / 2) ·
𝑋) + -((3 / 2) · (1
/ 6))) − (𝑋 + ((1 /
4) − (1 / 2))))) |
216 | | subdir 10343 |
. . . . . . . . . . . . . . 15
⊢ (((3 / 2)
∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑋 ∈ ℂ) → (((3 / 2) − 1)
· 𝑋) = (((3 / 2)
· 𝑋) − (1
· 𝑋))) |
217 | 108, 60, 216 | mp3an12 1406 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ ℂ → (((3 / 2)
− 1) · 𝑋) =
(((3 / 2) · 𝑋)
− (1 · 𝑋))) |
218 | | divsubdir 10600 |
. . . . . . . . . . . . . . . . . 18
⊢ ((3
∈ ℂ ∧ 2 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0))
→ ((3 − 2) / 2) = ((3 / 2) − (2 / 2))) |
219 | 35, 85, 104, 218 | mp3an 1416 |
. . . . . . . . . . . . . . . . 17
⊢ ((3
− 2) / 2) = ((3 / 2) − (2 / 2)) |
220 | 95 | oveq1i 6559 |
. . . . . . . . . . . . . . . . 17
⊢ ((3
− 2) / 2) = (1 / 2) |
221 | | 2div2e1 11027 |
. . . . . . . . . . . . . . . . . 18
⊢ (2 / 2) =
1 |
222 | 221 | oveq2i 6560 |
. . . . . . . . . . . . . . . . 17
⊢ ((3 / 2)
− (2 / 2)) = ((3 / 2) − 1) |
223 | 219, 220,
222 | 3eqtr3ri 2641 |
. . . . . . . . . . . . . . . 16
⊢ ((3 / 2)
− 1) = (1 / 2) |
224 | 223 | oveq1i 6559 |
. . . . . . . . . . . . . . 15
⊢ (((3 / 2)
− 1) · 𝑋) =
((1 / 2) · 𝑋) |
225 | 224 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ ℂ → (((3 / 2)
− 1) · 𝑋) =
((1 / 2) · 𝑋)) |
226 | | mulid2 9917 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 ∈ ℂ → (1
· 𝑋) = 𝑋) |
227 | 226 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ ℂ → (((3 / 2)
· 𝑋) − (1
· 𝑋)) = (((3 / 2)
· 𝑋) − 𝑋)) |
228 | 217, 225,
227 | 3eqtr3rd 2653 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → (((3 / 2)
· 𝑋) − 𝑋) = ((1 / 2) · 𝑋)) |
229 | 228 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → ((((3 /
2) · 𝑋) −
𝑋) − 0) = (((1 / 2)
· 𝑋) −
0)) |
230 | | mulcl 9899 |
. . . . . . . . . . . . . 14
⊢ (((1 / 2)
∈ ℂ ∧ 𝑋
∈ ℂ) → ((1 / 2) · 𝑋) ∈ ℂ) |
231 | 69, 230 | mpan 702 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → ((1 / 2)
· 𝑋) ∈
ℂ) |
232 | 231 | subid1d 10260 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → (((1 / 2)
· 𝑋) − 0) =
((1 / 2) · 𝑋)) |
233 | 229, 232 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → ((((3 /
2) · 𝑋) −
𝑋) − 0) = ((1 / 2)
· 𝑋)) |
234 | 212, 215,
233 | 3eqtr3a 2668 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ → ((((3 /
2) · 𝑋) + -((3 / 2)
· (1 / 6))) − (𝑋 + ((1 / 4) − (1 / 2)))) = ((1 / 2)
· 𝑋)) |
235 | 176, 182,
234 | 3eqtr2d 2650 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℂ → (((3 / 2)
· (𝑋 − (1 /
6))) − ((1 / 4) + (𝑋
− (1 / 2)))) = ((1 / 2) · 𝑋)) |
236 | 235 | negeqd 10154 |
. . . . . . . 8
⊢ (𝑋 ∈ ℂ → -(((3 /
2) · (𝑋 − (1 /
6))) − ((1 / 4) + (𝑋
− (1 / 2)))) = -((1 / 2) · 𝑋)) |
237 | 171, 236 | eqtr3d 2646 |
. . . . . . 7
⊢ (𝑋 ∈ ℂ → (((1 / 4)
+ (𝑋 − (1 / 2)))
− ((3 / 2) · (𝑋 − (1 / 6)))) = -((1 / 2) ·
𝑋)) |
238 | 237 | oveq2d 6565 |
. . . . . 6
⊢ (𝑋 ∈ ℂ → (((3 / 2)
· (𝑋↑2)) + (((1
/ 4) + (𝑋 − (1 / 2)))
− ((3 / 2) · (𝑋 − (1 / 6))))) = (((3 / 2) ·
(𝑋↑2)) + -((1 / 2)
· 𝑋))) |
239 | 133, 231 | negsubd 10277 |
. . . . . 6
⊢ (𝑋 ∈ ℂ → (((3 / 2)
· (𝑋↑2)) + -((1
/ 2) · 𝑋)) = (((3 /
2) · (𝑋↑2))
− ((1 / 2) · 𝑋))) |
240 | 170, 238,
239 | 3eqtrd 2648 |
. . . . 5
⊢ (𝑋 ∈ ℂ →
(Σ𝑘 ∈
(0...1)((3C𝑘) ·
((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) + (((3 / 2) ·
(𝑋↑2)) − ((3 /
2) · (𝑋 − (1 /
6))))) = (((3 / 2) · (𝑋↑2)) − ((1 / 2) · 𝑋))) |
241 | 143, 144,
240 | 3eqtrd 2648 |
. . . 4
⊢ (𝑋 ∈ ℂ →
Σ𝑘 ∈ (0...(1 +
1))((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (((3 / 2) · (𝑋↑2)) − ((1 / 2)
· 𝑋))) |
242 | 8, 241 | syl5eq 2656 |
. . 3
⊢ (𝑋 ∈ ℂ →
Σ𝑘 ∈ (0...(3
− 1))((3C𝑘) ·
((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1))) = (((3 / 2) ·
(𝑋↑2)) − ((1 /
2) · 𝑋))) |
243 | 242 | oveq2d 6565 |
. 2
⊢ (𝑋 ∈ ℂ → ((𝑋↑3) − Σ𝑘 ∈ (0...(3 −
1))((3C𝑘) · ((𝑘 BernPoly 𝑋) / ((3 − 𝑘) + 1)))) = ((𝑋↑3) − (((3 / 2) · (𝑋↑2)) − ((1 / 2)
· 𝑋)))) |
244 | | expcl 12740 |
. . . 4
⊢ ((𝑋 ∈ ℂ ∧ 3 ∈
ℕ0) → (𝑋↑3) ∈ ℂ) |
245 | 1, 244 | mpan2 703 |
. . 3
⊢ (𝑋 ∈ ℂ → (𝑋↑3) ∈
ℂ) |
246 | 245, 133,
231 | subsubd 10299 |
. 2
⊢ (𝑋 ∈ ℂ → ((𝑋↑3) − (((3 / 2)
· (𝑋↑2))
− ((1 / 2) · 𝑋))) = (((𝑋↑3) − ((3 / 2) · (𝑋↑2))) + ((1 / 2) ·
𝑋))) |
247 | 3, 243, 246 | 3eqtrd 2648 |
1
⊢ (𝑋 ∈ ℂ → (3
BernPoly 𝑋) = (((𝑋↑3) − ((3 / 2)
· (𝑋↑2))) + ((1
/ 2) · 𝑋))) |