Step |
Hyp |
Ref |
Expression |
1 |
|
1nn0 |
⊢ 1 ∈ ℕ0 |
2 |
|
bpolyval |
⊢ ( ( 1 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( 1 BernPoly 𝑋 ) = ( ( 𝑋 ↑ 1 ) − Σ 𝑘 ∈ ( 0 ... ( 1 − 1 ) ) ( ( 1 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 1 − 𝑘 ) + 1 ) ) ) ) ) |
3 |
1 2
|
mpan |
⊢ ( 𝑋 ∈ ℂ → ( 1 BernPoly 𝑋 ) = ( ( 𝑋 ↑ 1 ) − Σ 𝑘 ∈ ( 0 ... ( 1 − 1 ) ) ( ( 1 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 1 − 𝑘 ) + 1 ) ) ) ) ) |
4 |
|
exp1 |
⊢ ( 𝑋 ∈ ℂ → ( 𝑋 ↑ 1 ) = 𝑋 ) |
5 |
|
1m1e0 |
⊢ ( 1 − 1 ) = 0 |
6 |
5
|
oveq2i |
⊢ ( 0 ... ( 1 − 1 ) ) = ( 0 ... 0 ) |
7 |
6
|
sumeq1i |
⊢ Σ 𝑘 ∈ ( 0 ... ( 1 − 1 ) ) ( ( 1 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 1 − 𝑘 ) + 1 ) ) ) = Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 1 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 1 − 𝑘 ) + 1 ) ) ) |
8 |
|
0z |
⊢ 0 ∈ ℤ |
9 |
|
bpoly0 |
⊢ ( 𝑋 ∈ ℂ → ( 0 BernPoly 𝑋 ) = 1 ) |
10 |
9
|
oveq1d |
⊢ ( 𝑋 ∈ ℂ → ( ( 0 BernPoly 𝑋 ) / 2 ) = ( 1 / 2 ) ) |
11 |
10
|
oveq2d |
⊢ ( 𝑋 ∈ ℂ → ( 1 · ( ( 0 BernPoly 𝑋 ) / 2 ) ) = ( 1 · ( 1 / 2 ) ) ) |
12 |
|
halfcn |
⊢ ( 1 / 2 ) ∈ ℂ |
13 |
12
|
mulid2i |
⊢ ( 1 · ( 1 / 2 ) ) = ( 1 / 2 ) |
14 |
11 13
|
eqtrdi |
⊢ ( 𝑋 ∈ ℂ → ( 1 · ( ( 0 BernPoly 𝑋 ) / 2 ) ) = ( 1 / 2 ) ) |
15 |
14 12
|
eqeltrdi |
⊢ ( 𝑋 ∈ ℂ → ( 1 · ( ( 0 BernPoly 𝑋 ) / 2 ) ) ∈ ℂ ) |
16 |
|
oveq2 |
⊢ ( 𝑘 = 0 → ( 1 C 𝑘 ) = ( 1 C 0 ) ) |
17 |
|
bcn0 |
⊢ ( 1 ∈ ℕ0 → ( 1 C 0 ) = 1 ) |
18 |
1 17
|
ax-mp |
⊢ ( 1 C 0 ) = 1 |
19 |
16 18
|
eqtrdi |
⊢ ( 𝑘 = 0 → ( 1 C 𝑘 ) = 1 ) |
20 |
|
oveq1 |
⊢ ( 𝑘 = 0 → ( 𝑘 BernPoly 𝑋 ) = ( 0 BernPoly 𝑋 ) ) |
21 |
|
oveq2 |
⊢ ( 𝑘 = 0 → ( 1 − 𝑘 ) = ( 1 − 0 ) ) |
22 |
|
1m0e1 |
⊢ ( 1 − 0 ) = 1 |
23 |
21 22
|
eqtrdi |
⊢ ( 𝑘 = 0 → ( 1 − 𝑘 ) = 1 ) |
24 |
23
|
oveq1d |
⊢ ( 𝑘 = 0 → ( ( 1 − 𝑘 ) + 1 ) = ( 1 + 1 ) ) |
25 |
|
df-2 |
⊢ 2 = ( 1 + 1 ) |
26 |
24 25
|
eqtr4di |
⊢ ( 𝑘 = 0 → ( ( 1 − 𝑘 ) + 1 ) = 2 ) |
27 |
20 26
|
oveq12d |
⊢ ( 𝑘 = 0 → ( ( 𝑘 BernPoly 𝑋 ) / ( ( 1 − 𝑘 ) + 1 ) ) = ( ( 0 BernPoly 𝑋 ) / 2 ) ) |
28 |
19 27
|
oveq12d |
⊢ ( 𝑘 = 0 → ( ( 1 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 1 − 𝑘 ) + 1 ) ) ) = ( 1 · ( ( 0 BernPoly 𝑋 ) / 2 ) ) ) |
29 |
28
|
fsum1 |
⊢ ( ( 0 ∈ ℤ ∧ ( 1 · ( ( 0 BernPoly 𝑋 ) / 2 ) ) ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 1 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 1 − 𝑘 ) + 1 ) ) ) = ( 1 · ( ( 0 BernPoly 𝑋 ) / 2 ) ) ) |
30 |
8 15 29
|
sylancr |
⊢ ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 1 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 1 − 𝑘 ) + 1 ) ) ) = ( 1 · ( ( 0 BernPoly 𝑋 ) / 2 ) ) ) |
31 |
30 14
|
eqtrd |
⊢ ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 1 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 1 − 𝑘 ) + 1 ) ) ) = ( 1 / 2 ) ) |
32 |
7 31
|
syl5eq |
⊢ ( 𝑋 ∈ ℂ → Σ 𝑘 ∈ ( 0 ... ( 1 − 1 ) ) ( ( 1 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 1 − 𝑘 ) + 1 ) ) ) = ( 1 / 2 ) ) |
33 |
4 32
|
oveq12d |
⊢ ( 𝑋 ∈ ℂ → ( ( 𝑋 ↑ 1 ) − Σ 𝑘 ∈ ( 0 ... ( 1 − 1 ) ) ( ( 1 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 1 − 𝑘 ) + 1 ) ) ) ) = ( 𝑋 − ( 1 / 2 ) ) ) |
34 |
3 33
|
eqtrd |
⊢ ( 𝑋 ∈ ℂ → ( 1 BernPoly 𝑋 ) = ( 𝑋 − ( 1 / 2 ) ) ) |