Step | Hyp | Ref
| Expression |
1 | | oveq1 7198 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → (𝑥↑𝑛) = (𝑋↑𝑛)) |
2 | 1 | oveq1d 7206 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑋 → ((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))) |
3 | 2 | csbeq2dv 3805 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → ⦋(♯‘dom
𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ⦋(♯‘dom
𝑔) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))) |
4 | 3 | mpteq2dv 5136 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝑔 ∈ V ↦
⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))) = (𝑔 ∈ V ↦
⦋(♯‘dom 𝑔) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))))) |
5 | | bpoly.1 |
. . . . . . . 8
⊢ 𝐺 = (𝑔 ∈ V ↦
⦋(♯‘dom 𝑔) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))) |
6 | 4, 5 | eqtr4di 2789 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑔 ∈ V ↦
⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))) = 𝐺) |
7 | | wrecseq3 8030 |
. . . . . . 7
⊢ ((𝑔 ∈ V ↦
⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))) = 𝐺 → wrecs( < , ℕ0,
(𝑔 ∈ V ↦
⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))))) = wrecs( < ,
ℕ0, 𝐺)) |
8 | 6, 7 | syl 17 |
. . . . . 6
⊢ (𝑥 = 𝑋 → wrecs( < , ℕ0,
(𝑔 ∈ V ↦
⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))))) = wrecs( < ,
ℕ0, 𝐺)) |
9 | | bpoly.2 |
. . . . . 6
⊢ 𝐹 = wrecs( < ,
ℕ0, 𝐺) |
10 | 8, 9 | eqtr4di 2789 |
. . . . 5
⊢ (𝑥 = 𝑋 → wrecs( < , ℕ0,
(𝑔 ∈ V ↦
⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))))) = 𝐹) |
11 | 10 | fveq1d 6697 |
. . . 4
⊢ (𝑥 = 𝑋 → (wrecs( < , ℕ0,
(𝑔 ∈ V ↦
⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚) = (𝐹‘𝑚)) |
12 | | fveq2 6695 |
. . . 4
⊢ (𝑚 = 𝑁 → (𝐹‘𝑚) = (𝐹‘𝑁)) |
13 | 11, 12 | sylan9eqr 2793 |
. . 3
⊢ ((𝑚 = 𝑁 ∧ 𝑥 = 𝑋) → (wrecs( < , ℕ0,
(𝑔 ∈ V ↦
⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚) = (𝐹‘𝑁)) |
14 | | df-bpoly 15572 |
. . 3
⊢ BernPoly
= (𝑚 ∈
ℕ0, 𝑥
∈ ℂ ↦ (wrecs( < , ℕ0, (𝑔 ∈ V ↦
⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚)) |
15 | | fvex 6708 |
. . 3
⊢ (𝐹‘𝑁) ∈ V |
16 | 13, 14, 15 | ovmpoa 7342 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (𝑁 BernPoly 𝑋) = (𝐹‘𝑁)) |
17 | | ltweuz 13499 |
. . . . 5
⊢ < We
(ℤ≥‘0) |
18 | | nn0uz 12441 |
. . . . . 6
⊢
ℕ0 = (ℤ≥‘0) |
19 | | weeq2 5525 |
. . . . . 6
⊢
(ℕ0 = (ℤ≥‘0) → ( < We
ℕ0 ↔ < We
(ℤ≥‘0))) |
20 | 18, 19 | ax-mp 5 |
. . . . 5
⊢ ( < We
ℕ0 ↔ < We
(ℤ≥‘0)) |
21 | 17, 20 | mpbir 234 |
. . . 4
⊢ < We
ℕ0 |
22 | | nn0ex 12061 |
. . . . 5
⊢
ℕ0 ∈ V |
23 | | exse 5499 |
. . . . 5
⊢
(ℕ0 ∈ V → < Se
ℕ0) |
24 | 22, 23 | ax-mp 5 |
. . . 4
⊢ < Se
ℕ0 |
25 | 21, 24, 9 | wfr2 8052 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (𝐹‘𝑁) = (𝐺‘(𝐹 ↾ Pred( < , ℕ0,
𝑁)))) |
26 | 25 | adantr 484 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (𝐹‘𝑁) = (𝐺‘(𝐹 ↾ Pred( < , ℕ0,
𝑁)))) |
27 | | prednn0 13201 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ Pred( < , ℕ0, 𝑁) = (0...(𝑁 − 1))) |
28 | 27 | adantr 484 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ Pred( < , ℕ0, 𝑁) = (0...(𝑁 − 1))) |
29 | 28 | reseq2d 5836 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (𝐹 ↾ Pred(
< , ℕ0, 𝑁)) = (𝐹 ↾ (0...(𝑁 − 1)))) |
30 | 29 | fveq2d 6699 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (𝐺‘(𝐹 ↾ Pred( < ,
ℕ0, 𝑁))) =
(𝐺‘(𝐹 ↾ (0...(𝑁 − 1))))) |
31 | 21, 24, 9 | wfrfun 8043 |
. . . . . 6
⊢ Fun 𝐹 |
32 | | ovex 7224 |
. . . . . 6
⊢
(0...(𝑁 − 1))
∈ V |
33 | | resfunexg 7009 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ (0...(𝑁 − 1)) ∈ V) →
(𝐹 ↾ (0...(𝑁 − 1))) ∈
V) |
34 | 31, 32, 33 | mp2an 692 |
. . . . 5
⊢ (𝐹 ↾ (0...(𝑁 − 1))) ∈ V |
35 | | dmeq 5757 |
. . . . . . . . . . 11
⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → dom 𝑔 = dom (𝐹 ↾ (0...(𝑁 − 1)))) |
36 | 21, 24, 9 | wfr1 8051 |
. . . . . . . . . . . . 13
⊢ 𝐹 Fn
ℕ0 |
37 | | fz0ssnn0 13172 |
. . . . . . . . . . . . 13
⊢
(0...(𝑁 − 1))
⊆ ℕ0 |
38 | | fnssres 6478 |
. . . . . . . . . . . . 13
⊢ ((𝐹 Fn ℕ0 ∧
(0...(𝑁 − 1)) ⊆
ℕ0) → (𝐹 ↾ (0...(𝑁 − 1))) Fn (0...(𝑁 − 1))) |
39 | 36, 37, 38 | mp2an 692 |
. . . . . . . . . . . 12
⊢ (𝐹 ↾ (0...(𝑁 − 1))) Fn (0...(𝑁 − 1)) |
40 | 39 | fndmi 6460 |
. . . . . . . . . . 11
⊢ dom
(𝐹 ↾ (0...(𝑁 − 1))) = (0...(𝑁 − 1)) |
41 | 35, 40 | eqtrdi 2787 |
. . . . . . . . . 10
⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → dom 𝑔 = (0...(𝑁 − 1))) |
42 | | fveq1 6694 |
. . . . . . . . . . . . 13
⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → (𝑔‘𝑘) = ((𝐹 ↾ (0...(𝑁 − 1)))‘𝑘)) |
43 | | fvres 6714 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0...(𝑁 − 1)) → ((𝐹 ↾ (0...(𝑁 − 1)))‘𝑘) = (𝐹‘𝑘)) |
44 | 42, 43 | sylan9eq 2791 |
. . . . . . . . . . . 12
⊢ ((𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝑔‘𝑘) = (𝐹‘𝑘)) |
45 | 44 | oveq1d 7206 |
. . . . . . . . . . 11
⊢ ((𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)) = ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1))) |
46 | 45 | oveq2d 7207 |
. . . . . . . . . 10
⊢ ((𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))) = ((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) |
47 | 41, 46 | sumeq12rdv 15236 |
. . . . . . . . 9
⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) |
48 | 47 | oveq2d 7207 |
. . . . . . . 8
⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → ((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1))))) |
49 | 48 | csbeq2dv 3805 |
. . . . . . 7
⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) →
⦋(♯‘dom 𝑔) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ⦋(♯‘dom
𝑔) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1))))) |
50 | 41 | fveq2d 6699 |
. . . . . . . 8
⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → (♯‘dom
𝑔) =
(♯‘(0...(𝑁
− 1)))) |
51 | 50 | csbeq1d 3802 |
. . . . . . 7
⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) →
⦋(♯‘dom 𝑔) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) =
⦋(♯‘(0...(𝑁 − 1))) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1))))) |
52 | 49, 51 | eqtrd 2771 |
. . . . . 6
⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) →
⦋(♯‘dom 𝑔) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))) =
⦋(♯‘(0...(𝑁 − 1))) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1))))) |
53 | | ovex 7224 |
. . . . . . 7
⊢ ((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) ∈ V |
54 | 53 | csbex 5189 |
. . . . . 6
⊢
⦋(♯‘(0...(𝑁 − 1))) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) ∈ V |
55 | 52, 5, 54 | fvmpt 6796 |
. . . . 5
⊢ ((𝐹 ↾ (0...(𝑁 − 1))) ∈ V → (𝐺‘(𝐹 ↾ (0...(𝑁 − 1)))) =
⦋(♯‘(0...(𝑁 − 1))) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1))))) |
56 | 34, 55 | ax-mp 5 |
. . . 4
⊢ (𝐺‘(𝐹 ↾ (0...(𝑁 − 1)))) =
⦋(♯‘(0...(𝑁 − 1))) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) |
57 | | nfcvd 2898 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ Ⅎ𝑛((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1))))) |
58 | | oveq2 7199 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (𝑋↑𝑛) = (𝑋↑𝑁)) |
59 | | oveq1 7198 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑁 → (𝑛C𝑘) = (𝑁C𝑘)) |
60 | | oveq1 7198 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑁 → (𝑛 − 𝑘) = (𝑁 − 𝑘)) |
61 | 60 | oveq1d 7206 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑁 → ((𝑛 − 𝑘) + 1) = ((𝑁 − 𝑘) + 1)) |
62 | 61 | oveq2d 7207 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑁 → ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)) = ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1))) |
63 | 59, 62 | oveq12d 7209 |
. . . . . . . . 9
⊢ (𝑛 = 𝑁 → ((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1))) = ((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1)))) |
64 | 63 | sumeq2sdv 15233 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1)))) |
65 | 58, 64 | oveq12d 7209 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → ((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1))))) |
66 | 57, 65 | csbiegf 3832 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ ⦋𝑁 /
𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1))))) |
67 | 66 | adantr 484 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ ⦋𝑁 /
𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1))))) |
68 | | nn0z 12165 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
69 | | fz01en 13105 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ →
(0...(𝑁 − 1)) ≈
(1...𝑁)) |
70 | 68, 69 | syl 17 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (0...(𝑁 − 1))
≈ (1...𝑁)) |
71 | | fzfi 13510 |
. . . . . . . . . 10
⊢
(0...(𝑁 − 1))
∈ Fin |
72 | | fzfi 13510 |
. . . . . . . . . 10
⊢
(1...𝑁) ∈
Fin |
73 | | hashen 13878 |
. . . . . . . . . 10
⊢
(((0...(𝑁 −
1)) ∈ Fin ∧ (1...𝑁) ∈ Fin) →
((♯‘(0...(𝑁
− 1))) = (♯‘(1...𝑁)) ↔ (0...(𝑁 − 1)) ≈ (1...𝑁))) |
74 | 71, 72, 73 | mp2an 692 |
. . . . . . . . 9
⊢
((♯‘(0...(𝑁 − 1))) = (♯‘(1...𝑁)) ↔ (0...(𝑁 − 1)) ≈ (1...𝑁)) |
75 | 70, 74 | sylibr 237 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (♯‘(0...(𝑁 − 1))) = (♯‘(1...𝑁))) |
76 | | hashfz1 13877 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (♯‘(1...𝑁)) = 𝑁) |
77 | 75, 76 | eqtrd 2771 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (♯‘(0...(𝑁 − 1))) = 𝑁) |
78 | 77 | adantr 484 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (♯‘(0...(𝑁 − 1))) = 𝑁) |
79 | 78 | csbeq1d 3802 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ ⦋(♯‘(0...(𝑁 − 1))) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ⦋𝑁 / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1))))) |
80 | | elfznn0 13170 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ0) |
81 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ 𝑋 ∈
ℂ) |
82 | | fveq2 6695 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑘 → (𝐹‘𝑚) = (𝐹‘𝑘)) |
83 | 11, 82 | sylan9eqr 2793 |
. . . . . . . . . . 11
⊢ ((𝑚 = 𝑘 ∧ 𝑥 = 𝑋) → (wrecs( < , ℕ0,
(𝑔 ∈ V ↦
⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚) = (𝐹‘𝑘)) |
84 | | fvex 6708 |
. . . . . . . . . . 11
⊢ (𝐹‘𝑘) ∈ V |
85 | 83, 14, 84 | ovmpoa 7342 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (𝑘 BernPoly 𝑋) = (𝐹‘𝑘)) |
86 | 80, 81, 85 | syl2anr 600 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝑘 BernPoly 𝑋) = (𝐹‘𝑘)) |
87 | 86 | oveq1d 7206 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)) = ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1))) |
88 | 87 | oveq2d 7207 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))) = ((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1)))) |
89 | 88 | sumeq2dv 15232 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ Σ𝑘 ∈
(0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1)))) |
90 | 89 | oveq2d 7207 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1))))) |
91 | 67, 79, 90 | 3eqtr4d 2781 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ ⦋(♯‘(0...(𝑁 − 1))) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))))) |
92 | 56, 91 | syl5eq 2783 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (𝐺‘(𝐹 ↾ (0...(𝑁 − 1)))) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))))) |
93 | 30, 92 | eqtrd 2771 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (𝐺‘(𝐹 ↾ Pred( < ,
ℕ0, 𝑁))) =
((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))))) |
94 | 16, 26, 93 | 3eqtrd 2775 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (𝑁 BernPoly 𝑋) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))))) |