Step | Hyp | Ref
| Expression |
1 | | fvex 6113 |
. . . . . 6
⊢
(#‘dom 𝑐)
∈ V |
2 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑛 = (#‘dom 𝑐) → (𝑋↑𝑛) = (𝑋↑(#‘dom 𝑐))) |
3 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑛 = (#‘dom 𝑐) → (𝑛C𝑚) = ((#‘dom 𝑐)C𝑚)) |
4 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑛 = (#‘dom 𝑐) → (𝑛 − 𝑚) = ((#‘dom 𝑐) − 𝑚)) |
5 | 4 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝑛 = (#‘dom 𝑐) → ((𝑛 − 𝑚) + 1) = (((#‘dom 𝑐) − 𝑚) + 1)) |
6 | 5 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑛 = (#‘dom 𝑐) → ((𝑐‘𝑚) / ((𝑛 − 𝑚) + 1)) = ((𝑐‘𝑚) / (((#‘dom 𝑐) − 𝑚) + 1))) |
7 | 3, 6 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑛 = (#‘dom 𝑐) → ((𝑛C𝑚) · ((𝑐‘𝑚) / ((𝑛 − 𝑚) + 1))) = (((#‘dom 𝑐)C𝑚) · ((𝑐‘𝑚) / (((#‘dom 𝑐) − 𝑚) + 1)))) |
8 | 7 | sumeq2sdv 14282 |
. . . . . . 7
⊢ (𝑛 = (#‘dom 𝑐) → Σ𝑚 ∈ dom 𝑐((𝑛C𝑚) · ((𝑐‘𝑚) / ((𝑛 − 𝑚) + 1))) = Σ𝑚 ∈ dom 𝑐(((#‘dom 𝑐)C𝑚) · ((𝑐‘𝑚) / (((#‘dom 𝑐) − 𝑚) + 1)))) |
9 | 2, 8 | oveq12d 6567 |
. . . . . 6
⊢ (𝑛 = (#‘dom 𝑐) → ((𝑋↑𝑛) − Σ𝑚 ∈ dom 𝑐((𝑛C𝑚) · ((𝑐‘𝑚) / ((𝑛 − 𝑚) + 1)))) = ((𝑋↑(#‘dom 𝑐)) − Σ𝑚 ∈ dom 𝑐(((#‘dom 𝑐)C𝑚) · ((𝑐‘𝑚) / (((#‘dom 𝑐) − 𝑚) + 1))))) |
10 | 1, 9 | csbie 3525 |
. . . . 5
⊢
⦋(#‘dom 𝑐) / 𝑛⦌((𝑋↑𝑛) − Σ𝑚 ∈ dom 𝑐((𝑛C𝑚) · ((𝑐‘𝑚) / ((𝑛 − 𝑚) + 1)))) = ((𝑋↑(#‘dom 𝑐)) − Σ𝑚 ∈ dom 𝑐(((#‘dom 𝑐)C𝑚) · ((𝑐‘𝑚) / (((#‘dom 𝑐) − 𝑚) + 1)))) |
11 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑘 → (𝑛C𝑚) = (𝑛C𝑘)) |
12 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑘 → (𝑐‘𝑚) = (𝑐‘𝑘)) |
13 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑘 → (𝑛 − 𝑚) = (𝑛 − 𝑘)) |
14 | 13 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑘 → ((𝑛 − 𝑚) + 1) = ((𝑛 − 𝑘) + 1)) |
15 | 12, 14 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑘 → ((𝑐‘𝑚) / ((𝑛 − 𝑚) + 1)) = ((𝑐‘𝑘) / ((𝑛 − 𝑘) + 1))) |
16 | 11, 15 | oveq12d 6567 |
. . . . . . . . 9
⊢ (𝑚 = 𝑘 → ((𝑛C𝑚) · ((𝑐‘𝑚) / ((𝑛 − 𝑚) + 1))) = ((𝑛C𝑘) · ((𝑐‘𝑘) / ((𝑛 − 𝑘) + 1)))) |
17 | 16 | cbvsumv 14274 |
. . . . . . . 8
⊢
Σ𝑚 ∈ dom
𝑐((𝑛C𝑚) · ((𝑐‘𝑚) / ((𝑛 − 𝑚) + 1))) = Σ𝑘 ∈ dom 𝑐((𝑛C𝑘) · ((𝑐‘𝑘) / ((𝑛 − 𝑘) + 1))) |
18 | | dmeq 5246 |
. . . . . . . . 9
⊢ (𝑐 = 𝑔 → dom 𝑐 = dom 𝑔) |
19 | | fveq1 6102 |
. . . . . . . . . . . 12
⊢ (𝑐 = 𝑔 → (𝑐‘𝑘) = (𝑔‘𝑘)) |
20 | 19 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝑐 = 𝑔 → ((𝑐‘𝑘) / ((𝑛 − 𝑘) + 1)) = ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))) |
21 | 20 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑐 = 𝑔 → ((𝑛C𝑘) · ((𝑐‘𝑘) / ((𝑛 − 𝑘) + 1))) = ((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))) |
22 | 21 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑐 = 𝑔 ∧ 𝑘 ∈ dom 𝑐) → ((𝑛C𝑘) · ((𝑐‘𝑘) / ((𝑛 − 𝑘) + 1))) = ((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))) |
23 | 18, 22 | sumeq12dv 14284 |
. . . . . . . 8
⊢ (𝑐 = 𝑔 → Σ𝑘 ∈ dom 𝑐((𝑛C𝑘) · ((𝑐‘𝑘) / ((𝑛 − 𝑘) + 1))) = Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))) |
24 | 17, 23 | syl5eq 2656 |
. . . . . . 7
⊢ (𝑐 = 𝑔 → Σ𝑚 ∈ dom 𝑐((𝑛C𝑚) · ((𝑐‘𝑚) / ((𝑛 − 𝑚) + 1))) = Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))) |
25 | 24 | oveq2d 6565 |
. . . . . 6
⊢ (𝑐 = 𝑔 → ((𝑋↑𝑛) − Σ𝑚 ∈ dom 𝑐((𝑛C𝑚) · ((𝑐‘𝑚) / ((𝑛 − 𝑚) + 1)))) = ((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))) |
26 | 25 | csbeq2dv 3944 |
. . . . 5
⊢ (𝑐 = 𝑔 → ⦋(#‘dom 𝑐) / 𝑛⦌((𝑋↑𝑛) − Σ𝑚 ∈ dom 𝑐((𝑛C𝑚) · ((𝑐‘𝑚) / ((𝑛 − 𝑚) + 1)))) = ⦋(#‘dom 𝑐) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))) |
27 | 10, 26 | syl5eqr 2658 |
. . . 4
⊢ (𝑐 = 𝑔 → ((𝑋↑(#‘dom 𝑐)) − Σ𝑚 ∈ dom 𝑐(((#‘dom 𝑐)C𝑚) · ((𝑐‘𝑚) / (((#‘dom 𝑐) − 𝑚) + 1)))) = ⦋(#‘dom 𝑐) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))) |
28 | 18 | fveq2d 6107 |
. . . . 5
⊢ (𝑐 = 𝑔 → (#‘dom 𝑐) = (#‘dom 𝑔)) |
29 | 28 | csbeq1d 3506 |
. . . 4
⊢ (𝑐 = 𝑔 → ⦋(#‘dom 𝑐) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ⦋(#‘dom 𝑔) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))) |
30 | 27, 29 | eqtrd 2644 |
. . 3
⊢ (𝑐 = 𝑔 → ((𝑋↑(#‘dom 𝑐)) − Σ𝑚 ∈ dom 𝑐(((#‘dom 𝑐)C𝑚) · ((𝑐‘𝑚) / (((#‘dom 𝑐) − 𝑚) + 1)))) = ⦋(#‘dom 𝑔) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))) |
31 | 30 | cbvmptv 4678 |
. 2
⊢ (𝑐 ∈ V ↦ ((𝑋↑(#‘dom 𝑐)) − Σ𝑚 ∈ dom 𝑐(((#‘dom 𝑐)C𝑚) · ((𝑐‘𝑚) / (((#‘dom 𝑐) − 𝑚) + 1))))) = (𝑔 ∈ V ↦ ⦋(#‘dom
𝑔) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))) |
32 | | eqid 2610 |
. 2
⊢ wrecs(
< , ℕ0, (𝑐 ∈ V ↦ ((𝑋↑(#‘dom 𝑐)) − Σ𝑚 ∈ dom 𝑐(((#‘dom 𝑐)C𝑚) · ((𝑐‘𝑚) / (((#‘dom 𝑐) − 𝑚) + 1)))))) = wrecs( < ,
ℕ0, (𝑐
∈ V ↦ ((𝑋↑(#‘dom 𝑐)) − Σ𝑚 ∈ dom 𝑐(((#‘dom 𝑐)C𝑚) · ((𝑐‘𝑚) / (((#‘dom 𝑐) − 𝑚) + 1)))))) |
33 | 31, 32 | bpolylem 14618 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (𝑁 BernPoly 𝑋) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))))) |