| Step | Hyp | Ref
| Expression |
| 1 | | oveq1 7438 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → (𝑥↑𝑛) = (𝑋↑𝑛)) |
| 2 | 1 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑋 → ((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))) |
| 3 | 2 | csbeq2dv 3906 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → ⦋(♯‘dom
𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ⦋(♯‘dom
𝑔) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))) |
| 4 | 3 | mpteq2dv 5244 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝑔 ∈ V ↦
⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))) = (𝑔 ∈ V ↦
⦋(♯‘dom 𝑔) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))))) |
| 5 | | bpoly.1 |
. . . . . . . 8
⊢ 𝐺 = (𝑔 ∈ V ↦
⦋(♯‘dom 𝑔) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))) |
| 6 | 4, 5 | eqtr4di 2795 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑔 ∈ V ↦
⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))) = 𝐺) |
| 7 | | wrecseq3 8345 |
. . . . . . 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 2795 |
. . . . 5
⊢ (𝑥 = 𝑋 → wrecs( < , ℕ0,
(𝑔 ∈ V ↦
⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))))) = 𝐹) |
| 11 | 10 | fveq1d 6908 |
. . . 4
⊢ (𝑥 = 𝑋 → (wrecs( < , ℕ0,
(𝑔 ∈ V ↦
⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚) = (𝐹‘𝑚)) |
| 12 | | fveq2 6906 |
. . . 4
⊢ (𝑚 = 𝑁 → (𝐹‘𝑚) = (𝐹‘𝑁)) |
| 13 | 11, 12 | sylan9eqr 2799 |
. . 3
⊢ ((𝑚 = 𝑁 ∧ 𝑥 = 𝑋) → (wrecs( < , ℕ0,
(𝑔 ∈ V ↦
⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚) = (𝐹‘𝑁)) |
| 14 | | df-bpoly 16083 |
. . 3
⊢ BernPoly
= (𝑚 ∈
ℕ0, 𝑥
∈ ℂ ↦ (wrecs( < , ℕ0, (𝑔 ∈ V ↦
⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚)) |
| 15 | | fvex 6919 |
. . 3
⊢ (𝐹‘𝑁) ∈ V |
| 16 | 13, 14, 15 | ovmpoa 7588 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (𝑁 BernPoly 𝑋) = (𝐹‘𝑁)) |
| 17 | | ltweuz 14002 |
. . . . 5
⊢ < We
(ℤ≥‘0) |
| 18 | | nn0uz 12920 |
. . . . . 6
⊢
ℕ0 = (ℤ≥‘0) |
| 19 | | weeq2 5673 |
. . . . . 6
⊢
(ℕ0 = (ℤ≥‘0) → ( < We
ℕ0 ↔ < We
(ℤ≥‘0))) |
| 20 | 18, 19 | ax-mp 5 |
. . . . 5
⊢ ( < We
ℕ0 ↔ < We
(ℤ≥‘0)) |
| 21 | 17, 20 | mpbir 231 |
. . . 4
⊢ < We
ℕ0 |
| 22 | | nn0ex 12532 |
. . . . 5
⊢
ℕ0 ∈ V |
| 23 | | exse 5645 |
. . . . 5
⊢
(ℕ0 ∈ V → < Se
ℕ0) |
| 24 | 22, 23 | ax-mp 5 |
. . . 4
⊢ < Se
ℕ0 |
| 25 | 9 | wfr2 8376 |
. . . 4
⊢ ((( <
We ℕ0 ∧ < Se ℕ0) ∧ 𝑁 ∈ ℕ0)
→ (𝐹‘𝑁) = (𝐺‘(𝐹 ↾ Pred( < , ℕ0,
𝑁)))) |
| 26 | 21, 24, 25 | mpanl12 702 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (𝐹‘𝑁) = (𝐺‘(𝐹 ↾ Pred( < , ℕ0,
𝑁)))) |
| 27 | 26 | adantr 480 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (𝐹‘𝑁) = (𝐺‘(𝐹 ↾ Pred( < , ℕ0,
𝑁)))) |
| 28 | | prednn0 13692 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ Pred( < , ℕ0, 𝑁) = (0...(𝑁 − 1))) |
| 29 | 28 | adantr 480 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ Pred( < , ℕ0, 𝑁) = (0...(𝑁 − 1))) |
| 30 | 29 | reseq2d 5997 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (𝐹 ↾ Pred(
< , ℕ0, 𝑁)) = (𝐹 ↾ (0...(𝑁 − 1)))) |
| 31 | 30 | fveq2d 6910 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (𝐺‘(𝐹 ↾ Pred( < ,
ℕ0, 𝑁))) =
(𝐺‘(𝐹 ↾ (0...(𝑁 − 1))))) |
| 32 | 9 | wfrfun 8372 |
. . . . . . 7
⊢ (( <
We ℕ0 ∧ < Se ℕ0) → Fun 𝐹) |
| 33 | 21, 24, 32 | mp2an 692 |
. . . . . 6
⊢ Fun 𝐹 |
| 34 | | ovex 7464 |
. . . . . 6
⊢
(0...(𝑁 − 1))
∈ V |
| 35 | | resfunexg 7235 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ (0...(𝑁 − 1)) ∈ V) →
(𝐹 ↾ (0...(𝑁 − 1))) ∈
V) |
| 36 | 33, 34, 35 | mp2an 692 |
. . . . 5
⊢ (𝐹 ↾ (0...(𝑁 − 1))) ∈ V |
| 37 | | dmeq 5914 |
. . . . . . . . 9
⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → dom 𝑔 = dom (𝐹 ↾ (0...(𝑁 − 1)))) |
| 38 | 9 | wfr1 8375 |
. . . . . . . . . . . 12
⊢ (( <
We ℕ0 ∧ < Se ℕ0) → 𝐹 Fn
ℕ0) |
| 39 | 21, 24, 38 | mp2an 692 |
. . . . . . . . . . 11
⊢ 𝐹 Fn
ℕ0 |
| 40 | | fz0ssnn0 13662 |
. . . . . . . . . . 11
⊢
(0...(𝑁 − 1))
⊆ ℕ0 |
| 41 | | fnssres 6691 |
. . . . . . . . . . 11
⊢ ((𝐹 Fn ℕ0 ∧
(0...(𝑁 − 1)) ⊆
ℕ0) → (𝐹 ↾ (0...(𝑁 − 1))) Fn (0...(𝑁 − 1))) |
| 42 | 39, 40, 41 | mp2an 692 |
. . . . . . . . . 10
⊢ (𝐹 ↾ (0...(𝑁 − 1))) Fn (0...(𝑁 − 1)) |
| 43 | 42 | fndmi 6672 |
. . . . . . . . 9
⊢ dom
(𝐹 ↾ (0...(𝑁 − 1))) = (0...(𝑁 − 1)) |
| 44 | 37, 43 | eqtrdi 2793 |
. . . . . . . 8
⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → dom 𝑔 = (0...(𝑁 − 1))) |
| 45 | 44 | fveq2d 6910 |
. . . . . . 7
⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → (♯‘dom
𝑔) =
(♯‘(0...(𝑁
− 1)))) |
| 46 | | fveq1 6905 |
. . . . . . . . . . . 12
⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → (𝑔‘𝑘) = ((𝐹 ↾ (0...(𝑁 − 1)))‘𝑘)) |
| 47 | | fvres 6925 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (0...(𝑁 − 1)) → ((𝐹 ↾ (0...(𝑁 − 1)))‘𝑘) = (𝐹‘𝑘)) |
| 48 | 46, 47 | sylan9eq 2797 |
. . . . . . . . . . 11
⊢ ((𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝑔‘𝑘) = (𝐹‘𝑘)) |
| 49 | 48 | oveq1d 7446 |
. . . . . . . . . 10
⊢ ((𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)) = ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1))) |
| 50 | 49 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))) = ((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) |
| 51 | 44, 50 | sumeq12rdv 15743 |
. . . . . . . 8
⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) |
| 52 | 51 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) → ((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1))))) |
| 53 | 45, 52 | csbeq12dv 3908 |
. . . . . 6
⊢ (𝑔 = (𝐹 ↾ (0...(𝑁 − 1))) →
⦋(♯‘dom 𝑔) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1)))) =
⦋(♯‘(0...(𝑁 − 1))) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1))))) |
| 54 | | ovex 7464 |
. . . . . . 7
⊢ ((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) ∈ V |
| 55 | 54 | csbex 5311 |
. . . . . 6
⊢
⦋(♯‘(0...(𝑁 − 1))) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) ∈ V |
| 56 | 53, 5, 55 | fvmpt 7016 |
. . . . 5
⊢ ((𝐹 ↾ (0...(𝑁 − 1))) ∈ V → (𝐺‘(𝐹 ↾ (0...(𝑁 − 1)))) =
⦋(♯‘(0...(𝑁 − 1))) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1))))) |
| 57 | 36, 56 | ax-mp 5 |
. . . 4
⊢ (𝐺‘(𝐹 ↾ (0...(𝑁 − 1)))) =
⦋(♯‘(0...(𝑁 − 1))) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) |
| 58 | | nfcvd 2906 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ Ⅎ𝑛((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1))))) |
| 59 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (𝑋↑𝑛) = (𝑋↑𝑁)) |
| 60 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑁 → (𝑛C𝑘) = (𝑁C𝑘)) |
| 61 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑁 → (𝑛 − 𝑘) = (𝑁 − 𝑘)) |
| 62 | 61 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑁 → ((𝑛 − 𝑘) + 1) = ((𝑁 − 𝑘) + 1)) |
| 63 | 62 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑁 → ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)) = ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1))) |
| 64 | 60, 63 | oveq12d 7449 |
. . . . . . . . 9
⊢ (𝑛 = 𝑁 → ((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1))) = ((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1)))) |
| 65 | 64 | sumeq2sdv 15739 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1)))) |
| 66 | 59, 65 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → ((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1))))) |
| 67 | 58, 66 | csbiegf 3932 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ ⦋𝑁 /
𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1))))) |
| 68 | 67 | adantr 480 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ ⦋𝑁 /
𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1))))) |
| 69 | | nn0z 12638 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
| 70 | | fz01en 13592 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ →
(0...(𝑁 − 1)) ≈
(1...𝑁)) |
| 71 | 69, 70 | syl 17 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (0...(𝑁 − 1))
≈ (1...𝑁)) |
| 72 | | fzfi 14013 |
. . . . . . . . . 10
⊢
(0...(𝑁 − 1))
∈ Fin |
| 73 | | fzfi 14013 |
. . . . . . . . . 10
⊢
(1...𝑁) ∈
Fin |
| 74 | | hashen 14386 |
. . . . . . . . . 10
⊢
(((0...(𝑁 −
1)) ∈ Fin ∧ (1...𝑁) ∈ Fin) →
((♯‘(0...(𝑁
− 1))) = (♯‘(1...𝑁)) ↔ (0...(𝑁 − 1)) ≈ (1...𝑁))) |
| 75 | 72, 73, 74 | mp2an 692 |
. . . . . . . . 9
⊢
((♯‘(0...(𝑁 − 1))) = (♯‘(1...𝑁)) ↔ (0...(𝑁 − 1)) ≈ (1...𝑁)) |
| 76 | 71, 75 | sylibr 234 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (♯‘(0...(𝑁 − 1))) = (♯‘(1...𝑁))) |
| 77 | | hashfz1 14385 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (♯‘(1...𝑁)) = 𝑁) |
| 78 | 76, 77 | eqtrd 2777 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (♯‘(0...(𝑁 − 1))) = 𝑁) |
| 79 | 78 | adantr 480 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (♯‘(0...(𝑁 − 1))) = 𝑁) |
| 80 | 79 | csbeq1d 3903 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ ⦋(♯‘(0...(𝑁 − 1))) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ⦋𝑁 / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1))))) |
| 81 | | elfznn0 13660 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ0) |
| 82 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ 𝑋 ∈
ℂ) |
| 83 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑘 → (𝐹‘𝑚) = (𝐹‘𝑘)) |
| 84 | 11, 83 | sylan9eqr 2799 |
. . . . . . . . . . 11
⊢ ((𝑚 = 𝑘 ∧ 𝑥 = 𝑋) → (wrecs( < , ℕ0,
(𝑔 ∈ V ↦
⦋(♯‘dom 𝑔) / 𝑛⦌((𝑥↑𝑛) − Σ𝑘 ∈ dom 𝑔((𝑛C𝑘) · ((𝑔‘𝑘) / ((𝑛 − 𝑘) + 1))))))‘𝑚) = (𝐹‘𝑘)) |
| 85 | | fvex 6919 |
. . . . . . . . . . 11
⊢ (𝐹‘𝑘) ∈ V |
| 86 | 84, 14, 85 | ovmpoa 7588 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (𝑘 BernPoly 𝑋) = (𝐹‘𝑘)) |
| 87 | 81, 82, 86 | syl2anr 597 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝑘 BernPoly 𝑋) = (𝐹‘𝑘)) |
| 88 | 87 | oveq1d 7446 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)) = ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1))) |
| 89 | 88 | oveq2d 7447 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))) = ((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1)))) |
| 90 | 89 | sumeq2dv 15738 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ Σ𝑘 ∈
(0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1)))) |
| 91 | 90 | oveq2d 7447 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝐹‘𝑘) / ((𝑁 − 𝑘) + 1))))) |
| 92 | 68, 80, 91 | 3eqtr4d 2787 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ ⦋(♯‘(0...(𝑁 − 1))) / 𝑛⦌((𝑋↑𝑛) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑛C𝑘) · ((𝐹‘𝑘) / ((𝑛 − 𝑘) + 1)))) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))))) |
| 93 | 57, 92 | eqtrid 2789 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (𝐺‘(𝐹 ↾ (0...(𝑁 − 1)))) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))))) |
| 94 | 31, 93 | eqtrd 2777 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (𝐺‘(𝐹 ↾ Pred( < ,
ℕ0, 𝑁))) =
((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))))) |
| 95 | 16, 27, 94 | 3eqtrd 2781 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (𝑁 BernPoly 𝑋) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))))) |