Step | Hyp | Ref
| Expression |
1 | | 2nn0 12233 |
. . 3
⊢ 2 ∈
ℕ0 |
2 | | bpolyval 15740 |
. . 3
⊢ ((2
∈ ℕ0 ∧ 𝑋 ∈ ℂ) → (2 BernPoly 𝑋) = ((𝑋↑2) − Σ𝑘 ∈ (0...(2 − 1))((2C𝑘) · ((𝑘 BernPoly 𝑋) / ((2 − 𝑘) + 1))))) |
3 | 1, 2 | mpan 686 |
. 2
⊢ (𝑋 ∈ ℂ → (2
BernPoly 𝑋) = ((𝑋↑2) − Σ𝑘 ∈ (0...(2 −
1))((2C𝑘) · ((𝑘 BernPoly 𝑋) / ((2 − 𝑘) + 1))))) |
4 | | 2m1e1 12082 |
. . . . . . 7
⊢ (2
− 1) = 1 |
5 | | 0p1e1 12078 |
. . . . . . 7
⊢ (0 + 1) =
1 |
6 | 4, 5 | eqtr4i 2770 |
. . . . . 6
⊢ (2
− 1) = (0 + 1) |
7 | 6 | oveq2i 7279 |
. . . . 5
⊢ (0...(2
− 1)) = (0...(0 + 1)) |
8 | 7 | sumeq1i 15391 |
. . . 4
⊢
Σ𝑘 ∈
(0...(2 − 1))((2C𝑘)
· ((𝑘 BernPoly 𝑋) / ((2 − 𝑘) + 1))) = Σ𝑘 ∈ (0...(0 + 1))((2C𝑘) · ((𝑘 BernPoly 𝑋) / ((2 − 𝑘) + 1))) |
9 | | 0nn0 12231 |
. . . . . . . . 9
⊢ 0 ∈
ℕ0 |
10 | | nn0uz 12602 |
. . . . . . . . 9
⊢
ℕ0 = (ℤ≥‘0) |
11 | 9, 10 | eleqtri 2838 |
. . . . . . . 8
⊢ 0 ∈
(ℤ≥‘0) |
12 | 11 | a1i 11 |
. . . . . . 7
⊢ (𝑋 ∈ ℂ → 0 ∈
(ℤ≥‘0)) |
13 | | 0z 12313 |
. . . . . . . . . . 11
⊢ 0 ∈
ℤ |
14 | | fzpr 13293 |
. . . . . . . . . . 11
⊢ (0 ∈
ℤ → (0...(0 + 1)) = {0, (0 + 1)}) |
15 | 13, 14 | ax-mp 5 |
. . . . . . . . . 10
⊢ (0...(0 +
1)) = {0, (0 + 1)} |
16 | 15 | eleq2i 2831 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...(0 + 1)) ↔
𝑘 ∈ {0, (0 +
1)}) |
17 | | vex 3434 |
. . . . . . . . . 10
⊢ 𝑘 ∈ V |
18 | 17 | elpr 4589 |
. . . . . . . . 9
⊢ (𝑘 ∈ {0, (0 + 1)} ↔
(𝑘 = 0 ∨ 𝑘 = (0 + 1))) |
19 | 16, 18 | bitri 274 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...(0 + 1)) ↔
(𝑘 = 0 ∨ 𝑘 = (0 + 1))) |
20 | | oveq2 7276 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 0 → (2C𝑘) = (2C0)) |
21 | | bcn0 14005 |
. . . . . . . . . . . . . 14
⊢ (2 ∈
ℕ0 → (2C0) = 1) |
22 | 1, 21 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (2C0) =
1 |
23 | 20, 22 | eqtrdi 2795 |
. . . . . . . . . . . 12
⊢ (𝑘 = 0 → (2C𝑘) = 1) |
24 | | oveq1 7275 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 0 → (𝑘 BernPoly 𝑋) = (0 BernPoly 𝑋)) |
25 | | oveq2 7276 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 0 → (2 − 𝑘) = (2 −
0)) |
26 | 25 | oveq1d 7283 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 0 → ((2 − 𝑘) + 1) = ((2 − 0) +
1)) |
27 | | 2cn 12031 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℂ |
28 | 27 | subid1i 11276 |
. . . . . . . . . . . . . . . 16
⊢ (2
− 0) = 2 |
29 | 28 | oveq1i 7278 |
. . . . . . . . . . . . . . 15
⊢ ((2
− 0) + 1) = (2 + 1) |
30 | | df-3 12020 |
. . . . . . . . . . . . . . 15
⊢ 3 = (2 +
1) |
31 | 29, 30 | eqtr4i 2770 |
. . . . . . . . . . . . . 14
⊢ ((2
− 0) + 1) = 3 |
32 | 26, 31 | eqtrdi 2795 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 0 → ((2 − 𝑘) + 1) = 3) |
33 | 24, 32 | oveq12d 7286 |
. . . . . . . . . . . 12
⊢ (𝑘 = 0 → ((𝑘 BernPoly 𝑋) / ((2 − 𝑘) + 1)) = ((0 BernPoly 𝑋) / 3)) |
34 | 23, 33 | oveq12d 7286 |
. . . . . . . . . . 11
⊢ (𝑘 = 0 → ((2C𝑘) · ((𝑘 BernPoly 𝑋) / ((2 − 𝑘) + 1))) = (1 · ((0 BernPoly 𝑋) / 3))) |
35 | | bpoly0 15741 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ ℂ → (0
BernPoly 𝑋) =
1) |
36 | 35 | oveq1d 7283 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → ((0
BernPoly 𝑋) / 3) = (1 /
3)) |
37 | 36 | oveq2d 7284 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → (1
· ((0 BernPoly 𝑋) /
3)) = (1 · (1 / 3))) |
38 | | 3cn 12037 |
. . . . . . . . . . . . . 14
⊢ 3 ∈
ℂ |
39 | | 3ne0 12062 |
. . . . . . . . . . . . . 14
⊢ 3 ≠
0 |
40 | 38, 39 | reccli 11688 |
. . . . . . . . . . . . 13
⊢ (1 / 3)
∈ ℂ |
41 | 40 | mulid2i 10964 |
. . . . . . . . . . . 12
⊢ (1
· (1 / 3)) = (1 / 3) |
42 | 37, 41 | eqtrdi 2795 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → (1
· ((0 BernPoly 𝑋) /
3)) = (1 / 3)) |
43 | 34, 42 | sylan9eqr 2801 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 = 0) → ((2C𝑘) · ((𝑘 BernPoly 𝑋) / ((2 − 𝑘) + 1))) = (1 / 3)) |
44 | 43, 40 | eqeltrdi 2848 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 = 0) → ((2C𝑘) · ((𝑘 BernPoly 𝑋) / ((2 − 𝑘) + 1))) ∈ ℂ) |
45 | 5 | eqeq2i 2752 |
. . . . . . . . . . . 12
⊢ (𝑘 = (0 + 1) ↔ 𝑘 = 1) |
46 | | oveq2 7276 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 1 → (2C𝑘) = (2C1)) |
47 | | bcn1 14008 |
. . . . . . . . . . . . . . 15
⊢ (2 ∈
ℕ0 → (2C1) = 2) |
48 | 1, 47 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (2C1) =
2 |
49 | 46, 48 | eqtrdi 2795 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 1 → (2C𝑘) = 2) |
50 | | oveq1 7275 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 1 → (𝑘 BernPoly 𝑋) = (1 BernPoly 𝑋)) |
51 | | oveq2 7276 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 1 → (2 − 𝑘) = (2 −
1)) |
52 | 51 | oveq1d 7283 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 1 → ((2 − 𝑘) + 1) = ((2 − 1) +
1)) |
53 | | ax-1cn 10913 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℂ |
54 | | npcan 11213 |
. . . . . . . . . . . . . . . 16
⊢ ((2
∈ ℂ ∧ 1 ∈ ℂ) → ((2 − 1) + 1) =
2) |
55 | 27, 53, 54 | mp2an 688 |
. . . . . . . . . . . . . . 15
⊢ ((2
− 1) + 1) = 2 |
56 | 52, 55 | eqtrdi 2795 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 1 → ((2 − 𝑘) + 1) = 2) |
57 | 50, 56 | oveq12d 7286 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 1 → ((𝑘 BernPoly 𝑋) / ((2 − 𝑘) + 1)) = ((1 BernPoly 𝑋) / 2)) |
58 | 49, 57 | oveq12d 7286 |
. . . . . . . . . . . 12
⊢ (𝑘 = 1 → ((2C𝑘) · ((𝑘 BernPoly 𝑋) / ((2 − 𝑘) + 1))) = (2 · ((1 BernPoly 𝑋) / 2))) |
59 | 45, 58 | sylbi 216 |
. . . . . . . . . . 11
⊢ (𝑘 = (0 + 1) → ((2C𝑘) · ((𝑘 BernPoly 𝑋) / ((2 − 𝑘) + 1))) = (2 · ((1 BernPoly 𝑋) / 2))) |
60 | | bpoly1 15742 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ ℂ → (1
BernPoly 𝑋) = (𝑋 − (1 /
2))) |
61 | 60 | oveq1d 7283 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → ((1
BernPoly 𝑋) / 2) = ((𝑋 − (1 / 2)) /
2)) |
62 | 61 | oveq2d 7284 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → (2
· ((1 BernPoly 𝑋) /
2)) = (2 · ((𝑋
− (1 / 2)) / 2))) |
63 | | halfcn 12171 |
. . . . . . . . . . . . . 14
⊢ (1 / 2)
∈ ℂ |
64 | | subcl 11203 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ ℂ ∧ (1 / 2)
∈ ℂ) → (𝑋
− (1 / 2)) ∈ ℂ) |
65 | 63, 64 | mpan2 687 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ → (𝑋 − (1 / 2)) ∈
ℂ) |
66 | | 2ne0 12060 |
. . . . . . . . . . . . . 14
⊢ 2 ≠
0 |
67 | | divcan2 11624 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 − (1 / 2)) ∈ ℂ
∧ 2 ∈ ℂ ∧ 2 ≠ 0) → (2 · ((𝑋 − (1 / 2)) / 2)) = (𝑋 − (1 / 2))) |
68 | 27, 66, 67 | mp3an23 1451 |
. . . . . . . . . . . . 13
⊢ ((𝑋 − (1 / 2)) ∈ ℂ
→ (2 · ((𝑋
− (1 / 2)) / 2)) = (𝑋
− (1 / 2))) |
69 | 65, 68 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℂ → (2
· ((𝑋 − (1 /
2)) / 2)) = (𝑋 − (1 /
2))) |
70 | 62, 69 | eqtrd 2779 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → (2
· ((1 BernPoly 𝑋) /
2)) = (𝑋 − (1 /
2))) |
71 | 59, 70 | sylan9eqr 2801 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 = (0 + 1)) → ((2C𝑘) · ((𝑘 BernPoly 𝑋) / ((2 − 𝑘) + 1))) = (𝑋 − (1 / 2))) |
72 | 65 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 = (0 + 1)) → (𝑋 − (1 / 2)) ∈
ℂ) |
73 | 71, 72 | eqeltrd 2840 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 = (0 + 1)) → ((2C𝑘) · ((𝑘 BernPoly 𝑋) / ((2 − 𝑘) + 1))) ∈ ℂ) |
74 | 44, 73 | jaodan 954 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℂ ∧ (𝑘 = 0 ∨ 𝑘 = (0 + 1))) → ((2C𝑘) · ((𝑘 BernPoly 𝑋) / ((2 − 𝑘) + 1))) ∈ ℂ) |
75 | 19, 74 | sylan2b 593 |
. . . . . . 7
⊢ ((𝑋 ∈ ℂ ∧ 𝑘 ∈ (0...(0 + 1))) →
((2C𝑘) · ((𝑘 BernPoly 𝑋) / ((2 − 𝑘) + 1))) ∈ ℂ) |
76 | 12, 75, 59 | fsump1 15449 |
. . . . . 6
⊢ (𝑋 ∈ ℂ →
Σ𝑘 ∈ (0...(0 +
1))((2C𝑘) · ((𝑘 BernPoly 𝑋) / ((2 − 𝑘) + 1))) = (Σ𝑘 ∈ (0...0)((2C𝑘) · ((𝑘 BernPoly 𝑋) / ((2 − 𝑘) + 1))) + (2 · ((1 BernPoly 𝑋) / 2)))) |
77 | 42, 40 | eqeltrdi 2848 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℂ → (1
· ((0 BernPoly 𝑋) /
3)) ∈ ℂ) |
78 | 34 | fsum1 15440 |
. . . . . . . . 9
⊢ ((0
∈ ℤ ∧ (1 · ((0 BernPoly 𝑋) / 3)) ∈ ℂ) → Σ𝑘 ∈ (0...0)((2C𝑘) · ((𝑘 BernPoly 𝑋) / ((2 − 𝑘) + 1))) = (1 · ((0 BernPoly 𝑋) / 3))) |
79 | 13, 77, 78 | sylancr 586 |
. . . . . . . 8
⊢ (𝑋 ∈ ℂ →
Σ𝑘 ∈
(0...0)((2C𝑘) ·
((𝑘 BernPoly 𝑋) / ((2 − 𝑘) + 1))) = (1 · ((0
BernPoly 𝑋) /
3))) |
80 | 79, 42 | eqtrd 2779 |
. . . . . . 7
⊢ (𝑋 ∈ ℂ →
Σ𝑘 ∈
(0...0)((2C𝑘) ·
((𝑘 BernPoly 𝑋) / ((2 − 𝑘) + 1))) = (1 /
3)) |
81 | 80, 70 | oveq12d 7286 |
. . . . . 6
⊢ (𝑋 ∈ ℂ →
(Σ𝑘 ∈
(0...0)((2C𝑘) ·
((𝑘 BernPoly 𝑋) / ((2 − 𝑘) + 1))) + (2 · ((1
BernPoly 𝑋) / 2))) = ((1 /
3) + (𝑋 − (1 /
2)))) |
82 | 76, 81 | eqtrd 2779 |
. . . . 5
⊢ (𝑋 ∈ ℂ →
Σ𝑘 ∈ (0...(0 +
1))((2C𝑘) · ((𝑘 BernPoly 𝑋) / ((2 − 𝑘) + 1))) = ((1 / 3) + (𝑋 − (1 / 2)))) |
83 | | addsub12 11217 |
. . . . . . 7
⊢ (((1 / 3)
∈ ℂ ∧ 𝑋
∈ ℂ ∧ (1 / 2) ∈ ℂ) → ((1 / 3) + (𝑋 − (1 / 2))) = (𝑋 + ((1 / 3) − (1 /
2)))) |
84 | 40, 63, 83 | mp3an13 1450 |
. . . . . 6
⊢ (𝑋 ∈ ℂ → ((1 / 3)
+ (𝑋 − (1 / 2))) =
(𝑋 + ((1 / 3) − (1 /
2)))) |
85 | 63, 40 | negsubdi2i 11290 |
. . . . . . . 8
⊢ -((1 / 2)
− (1 / 3)) = ((1 / 3) − (1 / 2)) |
86 | | halfthird 12562 |
. . . . . . . . 9
⊢ ((1 / 2)
− (1 / 3)) = (1 / 6) |
87 | 86 | negeqi 11197 |
. . . . . . . 8
⊢ -((1 / 2)
− (1 / 3)) = -(1 / 6) |
88 | 85, 87 | eqtr3i 2769 |
. . . . . . 7
⊢ ((1 / 3)
− (1 / 2)) = -(1 / 6) |
89 | 88 | oveq2i 7279 |
. . . . . 6
⊢ (𝑋 + ((1 / 3) − (1 / 2))) =
(𝑋 + -(1 /
6)) |
90 | 84, 89 | eqtrdi 2795 |
. . . . 5
⊢ (𝑋 ∈ ℂ → ((1 / 3)
+ (𝑋 − (1 / 2))) =
(𝑋 + -(1 /
6))) |
91 | | 6cn 12047 |
. . . . . . 7
⊢ 6 ∈
ℂ |
92 | | 6re 12046 |
. . . . . . . 8
⊢ 6 ∈
ℝ |
93 | | 6pos 12066 |
. . . . . . . 8
⊢ 0 <
6 |
94 | 92, 93 | gt0ne0ii 11494 |
. . . . . . 7
⊢ 6 ≠
0 |
95 | 91, 94 | reccli 11688 |
. . . . . 6
⊢ (1 / 6)
∈ ℂ |
96 | | negsub 11252 |
. . . . . 6
⊢ ((𝑋 ∈ ℂ ∧ (1 / 6)
∈ ℂ) → (𝑋 +
-(1 / 6)) = (𝑋 − (1 /
6))) |
97 | 95, 96 | mpan2 687 |
. . . . 5
⊢ (𝑋 ∈ ℂ → (𝑋 + -(1 / 6)) = (𝑋 − (1 /
6))) |
98 | 82, 90, 97 | 3eqtrd 2783 |
. . . 4
⊢ (𝑋 ∈ ℂ →
Σ𝑘 ∈ (0...(0 +
1))((2C𝑘) · ((𝑘 BernPoly 𝑋) / ((2 − 𝑘) + 1))) = (𝑋 − (1 / 6))) |
99 | 8, 98 | eqtrid 2791 |
. . 3
⊢ (𝑋 ∈ ℂ →
Σ𝑘 ∈ (0...(2
− 1))((2C𝑘) ·
((𝑘 BernPoly 𝑋) / ((2 − 𝑘) + 1))) = (𝑋 − (1 / 6))) |
100 | 99 | oveq2d 7284 |
. 2
⊢ (𝑋 ∈ ℂ → ((𝑋↑2) − Σ𝑘 ∈ (0...(2 −
1))((2C𝑘) · ((𝑘 BernPoly 𝑋) / ((2 − 𝑘) + 1)))) = ((𝑋↑2) − (𝑋 − (1 / 6)))) |
101 | | sqcl 13819 |
. . 3
⊢ (𝑋 ∈ ℂ → (𝑋↑2) ∈
ℂ) |
102 | | subsub 11234 |
. . . 4
⊢ (((𝑋↑2) ∈ ℂ ∧
𝑋 ∈ ℂ ∧ (1 /
6) ∈ ℂ) → ((𝑋↑2) − (𝑋 − (1 / 6))) = (((𝑋↑2) − 𝑋) + (1 / 6))) |
103 | 95, 102 | mp3an3 1448 |
. . 3
⊢ (((𝑋↑2) ∈ ℂ ∧
𝑋 ∈ ℂ) →
((𝑋↑2) − (𝑋 − (1 / 6))) = (((𝑋↑2) − 𝑋) + (1 / 6))) |
104 | 101, 103 | mpancom 684 |
. 2
⊢ (𝑋 ∈ ℂ → ((𝑋↑2) − (𝑋 − (1 / 6))) = (((𝑋↑2) − 𝑋) + (1 / 6))) |
105 | 3, 100, 104 | 3eqtrd 2783 |
1
⊢ (𝑋 ∈ ℂ → (2
BernPoly 𝑋) = (((𝑋↑2) − 𝑋) + (1 / 6))) |