Proof of Theorem bpolysum
| Step | Hyp | Ref
| Expression |
| 1 | | simpl 482 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ 𝑁 ∈
ℕ0) |
| 2 | | nn0uz 12920 |
. . . 4
⊢
ℕ0 = (ℤ≥‘0) |
| 3 | 1, 2 | eleqtrdi 2851 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ 𝑁 ∈
(ℤ≥‘0)) |
| 4 | | elfzelz 13564 |
. . . . . 6
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℤ) |
| 5 | | bccl 14361 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ ℤ)
→ (𝑁C𝑘) ∈
ℕ0) |
| 6 | 1, 4, 5 | syl2an 596 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
∧ 𝑘 ∈ (0...𝑁)) → (𝑁C𝑘) ∈
ℕ0) |
| 7 | 6 | nn0cnd 12589 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
∧ 𝑘 ∈ (0...𝑁)) → (𝑁C𝑘) ∈ ℂ) |
| 8 | | elfznn0 13660 |
. . . . . 6
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) |
| 9 | | simpr 484 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ 𝑋 ∈
ℂ) |
| 10 | | bpolycl 16088 |
. . . . . 6
⊢ ((𝑘 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (𝑘 BernPoly 𝑋) ∈
ℂ) |
| 11 | 8, 9, 10 | syl2anr 597 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
∧ 𝑘 ∈ (0...𝑁)) → (𝑘 BernPoly 𝑋) ∈ ℂ) |
| 12 | | fznn0sub 13596 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...𝑁) → (𝑁 − 𝑘) ∈
ℕ0) |
| 13 | 12 | adantl 481 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
∧ 𝑘 ∈ (0...𝑁)) → (𝑁 − 𝑘) ∈
ℕ0) |
| 14 | | nn0p1nn 12565 |
. . . . . . 7
⊢ ((𝑁 − 𝑘) ∈ ℕ0 → ((𝑁 − 𝑘) + 1) ∈ ℕ) |
| 15 | 13, 14 | syl 17 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
∧ 𝑘 ∈ (0...𝑁)) → ((𝑁 − 𝑘) + 1) ∈ ℕ) |
| 16 | 15 | nncnd 12282 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
∧ 𝑘 ∈ (0...𝑁)) → ((𝑁 − 𝑘) + 1) ∈ ℂ) |
| 17 | 15 | nnne0d 12316 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
∧ 𝑘 ∈ (0...𝑁)) → ((𝑁 − 𝑘) + 1) ≠ 0) |
| 18 | 11, 16, 17 | divcld 12043 |
. . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
∧ 𝑘 ∈ (0...𝑁)) → ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)) ∈ ℂ) |
| 19 | 7, 18 | mulcld 11281 |
. . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))) ∈ ℂ) |
| 20 | | oveq2 7439 |
. . . 4
⊢ (𝑘 = 𝑁 → (𝑁C𝑘) = (𝑁C𝑁)) |
| 21 | | oveq1 7438 |
. . . . 5
⊢ (𝑘 = 𝑁 → (𝑘 BernPoly 𝑋) = (𝑁 BernPoly 𝑋)) |
| 22 | | oveq2 7439 |
. . . . . 6
⊢ (𝑘 = 𝑁 → (𝑁 − 𝑘) = (𝑁 − 𝑁)) |
| 23 | 22 | oveq1d 7446 |
. . . . 5
⊢ (𝑘 = 𝑁 → ((𝑁 − 𝑘) + 1) = ((𝑁 − 𝑁) + 1)) |
| 24 | 21, 23 | oveq12d 7449 |
. . . 4
⊢ (𝑘 = 𝑁 → ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)) = ((𝑁 BernPoly 𝑋) / ((𝑁 − 𝑁) + 1))) |
| 25 | 20, 24 | oveq12d 7449 |
. . 3
⊢ (𝑘 = 𝑁 → ((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))) = ((𝑁C𝑁) · ((𝑁 BernPoly 𝑋) / ((𝑁 − 𝑁) + 1)))) |
| 26 | 3, 19, 25 | fsumm1 15787 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ Σ𝑘 ∈
(0...𝑁)((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))) = (Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))) + ((𝑁C𝑁) · ((𝑁 BernPoly 𝑋) / ((𝑁 − 𝑁) + 1))))) |
| 27 | | bcnn 14351 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (𝑁C𝑁) = 1) |
| 28 | 27 | adantr 480 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (𝑁C𝑁) = 1) |
| 29 | | nn0cn 12536 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
| 30 | 29 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ 𝑁 ∈
ℂ) |
| 31 | 30 | subidd 11608 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (𝑁 − 𝑁) = 0) |
| 32 | 31 | oveq1d 7446 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ ((𝑁 − 𝑁) + 1) = (0 +
1)) |
| 33 | | 0p1e1 12388 |
. . . . . . . 8
⊢ (0 + 1) =
1 |
| 34 | 32, 33 | eqtrdi 2793 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ ((𝑁 − 𝑁) + 1) = 1) |
| 35 | 34 | oveq2d 7447 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ ((𝑁 BernPoly 𝑋) / ((𝑁 − 𝑁) + 1)) = ((𝑁 BernPoly 𝑋) / 1)) |
| 36 | | bpolycl 16088 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (𝑁 BernPoly 𝑋) ∈
ℂ) |
| 37 | 36 | div1d 12035 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ ((𝑁 BernPoly 𝑋) / 1) = (𝑁 BernPoly 𝑋)) |
| 38 | 35, 37 | eqtrd 2777 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ ((𝑁 BernPoly 𝑋) / ((𝑁 − 𝑁) + 1)) = (𝑁 BernPoly 𝑋)) |
| 39 | 28, 38 | oveq12d 7449 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ ((𝑁C𝑁) · ((𝑁 BernPoly 𝑋) / ((𝑁 − 𝑁) + 1))) = (1 · (𝑁 BernPoly 𝑋))) |
| 40 | 36 | mullidd 11279 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (1 · (𝑁
BernPoly 𝑋)) = (𝑁 BernPoly 𝑋)) |
| 41 | 39, 40 | eqtrd 2777 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ ((𝑁C𝑁) · ((𝑁 BernPoly 𝑋) / ((𝑁 − 𝑁) + 1))) = (𝑁 BernPoly 𝑋)) |
| 42 | 41 | oveq2d 7447 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (Σ𝑘 ∈
(0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))) + ((𝑁C𝑁) · ((𝑁 BernPoly 𝑋) / ((𝑁 − 𝑁) + 1)))) = (Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))) + (𝑁 BernPoly 𝑋))) |
| 43 | | bpolyval 16085 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (𝑁 BernPoly 𝑋) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))))) |
| 44 | 43 | eqcomd 2743 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))) = (𝑁 BernPoly 𝑋)) |
| 45 | | expcl 14120 |
. . . . 5
⊢ ((𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (𝑋↑𝑁) ∈
ℂ) |
| 46 | 45 | ancoms 458 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (𝑋↑𝑁) ∈
ℂ) |
| 47 | | fzfid 14014 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (0...(𝑁 − 1))
∈ Fin) |
| 48 | | fzssp1 13607 |
. . . . . . . 8
⊢
(0...(𝑁 − 1))
⊆ (0...((𝑁 − 1)
+ 1)) |
| 49 | | ax-1cn 11213 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
| 50 | | npcan 11517 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 −
1) + 1) = 𝑁) |
| 51 | 30, 49, 50 | sylancl 586 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ ((𝑁 − 1) + 1)
= 𝑁) |
| 52 | 51 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (0...((𝑁 − 1)
+ 1)) = (0...𝑁)) |
| 53 | 48, 52 | sseqtrid 4026 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (0...(𝑁 − 1))
⊆ (0...𝑁)) |
| 54 | 53 | sselda 3983 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ (0...𝑁)) |
| 55 | 54, 19 | syldan 591 |
. . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))) ∈ ℂ) |
| 56 | 47, 55 | fsumcl 15769 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ Σ𝑘 ∈
(0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))) ∈ ℂ) |
| 57 | 46, 56, 36 | subaddd 11638 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))) = (𝑁 BernPoly 𝑋) ↔ (Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))) + (𝑁 BernPoly 𝑋)) = (𝑋↑𝑁))) |
| 58 | 44, 57 | mpbid 232 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (Σ𝑘 ∈
(0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))) + (𝑁 BernPoly 𝑋)) = (𝑋↑𝑁)) |
| 59 | 26, 42, 58 | 3eqtrd 2781 |
1
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ Σ𝑘 ∈
(0...𝑁)((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))) = (𝑋↑𝑁)) |