| Step | Hyp | Ref
| Expression |
| 1 | | nn0p1nn 12565 |
. . . 4
⊢ (𝐾 ∈ ℕ0
→ (𝐾 + 1) ∈
ℕ) |
| 2 | 1 | adantr 480 |
. . 3
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝐾 + 1) ∈ ℕ) |
| 3 | 2 | nncnd 12282 |
. 2
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝐾 + 1) ∈ ℂ) |
| 4 | | fzfid 14014 |
. . 3
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (0...𝑀) ∈ Fin) |
| 5 | | elfzelz 13564 |
. . . . 5
⊢ (𝑛 ∈ (0...𝑀) → 𝑛 ∈ ℤ) |
| 6 | 5 | zcnd 12723 |
. . . 4
⊢ (𝑛 ∈ (0...𝑀) → 𝑛 ∈ ℂ) |
| 7 | | simpl 482 |
. . . 4
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → 𝐾 ∈
ℕ0) |
| 8 | | expcl 14120 |
. . . 4
⊢ ((𝑛 ∈ ℂ ∧ 𝐾 ∈ ℕ0)
→ (𝑛↑𝐾) ∈
ℂ) |
| 9 | 6, 7, 8 | syl2anr 597 |
. . 3
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑛 ∈ (0...𝑀)) → (𝑛↑𝐾) ∈ ℂ) |
| 10 | 4, 9 | fsumcl 15769 |
. 2
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → Σ𝑛 ∈ (0...𝑀)(𝑛↑𝐾) ∈ ℂ) |
| 11 | 2 | nnne0d 12316 |
. 2
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝐾 + 1) ≠ 0) |
| 12 | 4, 3, 9 | fsummulc2 15820 |
. . 3
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → ((𝐾 + 1) · Σ𝑛 ∈ (0...𝑀)(𝑛↑𝐾)) = Σ𝑛 ∈ (0...𝑀)((𝐾 + 1) · (𝑛↑𝐾))) |
| 13 | | bpolydif 16091 |
. . . . . 6
⊢ (((𝐾 + 1) ∈ ℕ ∧ 𝑛 ∈ ℂ) → (((𝐾 + 1) BernPoly (𝑛 + 1)) − ((𝐾 + 1) BernPoly 𝑛)) = ((𝐾 + 1) · (𝑛↑((𝐾 + 1) − 1)))) |
| 14 | 2, 6, 13 | syl2an 596 |
. . . . 5
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑛 ∈ (0...𝑀)) → (((𝐾 + 1) BernPoly (𝑛 + 1)) − ((𝐾 + 1) BernPoly 𝑛)) = ((𝐾 + 1) · (𝑛↑((𝐾 + 1) − 1)))) |
| 15 | | nn0cn 12536 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℂ) |
| 16 | 15 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑛 ∈ (0...𝑀)) → 𝐾 ∈ ℂ) |
| 17 | | ax-1cn 11213 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
| 18 | | pncan 11514 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐾 + 1)
− 1) = 𝐾) |
| 19 | 16, 17, 18 | sylancl 586 |
. . . . . . 7
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑛 ∈ (0...𝑀)) → ((𝐾 + 1) − 1) = 𝐾) |
| 20 | 19 | oveq2d 7447 |
. . . . . 6
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑛 ∈ (0...𝑀)) → (𝑛↑((𝐾 + 1) − 1)) = (𝑛↑𝐾)) |
| 21 | 20 | oveq2d 7447 |
. . . . 5
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑛 ∈ (0...𝑀)) → ((𝐾 + 1) · (𝑛↑((𝐾 + 1) − 1))) = ((𝐾 + 1) · (𝑛↑𝐾))) |
| 22 | 14, 21 | eqtrd 2777 |
. . . 4
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑛 ∈ (0...𝑀)) → (((𝐾 + 1) BernPoly (𝑛 + 1)) − ((𝐾 + 1) BernPoly 𝑛)) = ((𝐾 + 1) · (𝑛↑𝐾))) |
| 23 | 22 | sumeq2dv 15738 |
. . 3
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → Σ𝑛 ∈ (0...𝑀)(((𝐾 + 1) BernPoly (𝑛 + 1)) − ((𝐾 + 1) BernPoly 𝑛)) = Σ𝑛 ∈ (0...𝑀)((𝐾 + 1) · (𝑛↑𝐾))) |
| 24 | | oveq2 7439 |
. . . 4
⊢ (𝑘 = 𝑛 → ((𝐾 + 1) BernPoly 𝑘) = ((𝐾 + 1) BernPoly 𝑛)) |
| 25 | | oveq2 7439 |
. . . 4
⊢ (𝑘 = (𝑛 + 1) → ((𝐾 + 1) BernPoly 𝑘) = ((𝐾 + 1) BernPoly (𝑛 + 1))) |
| 26 | | oveq2 7439 |
. . . 4
⊢ (𝑘 = 0 → ((𝐾 + 1) BernPoly 𝑘) = ((𝐾 + 1) BernPoly 0)) |
| 27 | | oveq2 7439 |
. . . 4
⊢ (𝑘 = (𝑀 + 1) → ((𝐾 + 1) BernPoly 𝑘) = ((𝐾 + 1) BernPoly (𝑀 + 1))) |
| 28 | | nn0z 12638 |
. . . . 5
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℤ) |
| 29 | 28 | adantl 481 |
. . . 4
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → 𝑀 ∈ ℤ) |
| 30 | | peano2nn0 12566 |
. . . . . 6
⊢ (𝑀 ∈ ℕ0
→ (𝑀 + 1) ∈
ℕ0) |
| 31 | 30 | adantl 481 |
. . . . 5
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝑀 + 1) ∈
ℕ0) |
| 32 | | nn0uz 12920 |
. . . . 5
⊢
ℕ0 = (ℤ≥‘0) |
| 33 | 31, 32 | eleqtrdi 2851 |
. . . 4
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝑀 + 1) ∈
(ℤ≥‘0)) |
| 34 | | peano2nn0 12566 |
. . . . . 6
⊢ (𝐾 ∈ ℕ0
→ (𝐾 + 1) ∈
ℕ0) |
| 35 | 34 | ad2antrr 726 |
. . . . 5
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑘 ∈ (0...(𝑀 + 1))) → (𝐾 + 1) ∈
ℕ0) |
| 36 | | elfznn0 13660 |
. . . . . . 7
⊢ (𝑘 ∈ (0...(𝑀 + 1)) → 𝑘 ∈ ℕ0) |
| 37 | 36 | adantl 481 |
. . . . . 6
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑘 ∈ (0...(𝑀 + 1))) → 𝑘 ∈ ℕ0) |
| 38 | 37 | nn0cnd 12589 |
. . . . 5
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑘 ∈ (0...(𝑀 + 1))) → 𝑘 ∈ ℂ) |
| 39 | | bpolycl 16088 |
. . . . 5
⊢ (((𝐾 + 1) ∈ ℕ0
∧ 𝑘 ∈ ℂ)
→ ((𝐾 + 1) BernPoly
𝑘) ∈
ℂ) |
| 40 | 35, 38, 39 | syl2anc 584 |
. . . 4
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑘 ∈ (0...(𝑀 + 1))) → ((𝐾 + 1) BernPoly 𝑘) ∈ ℂ) |
| 41 | 24, 25, 26, 27, 29, 33, 40 | telfsum2 15841 |
. . 3
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → Σ𝑛 ∈ (0...𝑀)(((𝐾 + 1) BernPoly (𝑛 + 1)) − ((𝐾 + 1) BernPoly 𝑛)) = (((𝐾 + 1) BernPoly (𝑀 + 1)) − ((𝐾 + 1) BernPoly 0))) |
| 42 | 12, 23, 41 | 3eqtr2d 2783 |
. 2
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → ((𝐾 + 1) · Σ𝑛 ∈ (0...𝑀)(𝑛↑𝐾)) = (((𝐾 + 1) BernPoly (𝑀 + 1)) − ((𝐾 + 1) BernPoly 0))) |
| 43 | 3, 10, 11, 42 | mvllmuld 12099 |
1
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → Σ𝑛 ∈ (0...𝑀)(𝑛↑𝐾) = ((((𝐾 + 1) BernPoly (𝑀 + 1)) − ((𝐾 + 1) BernPoly 0)) / (𝐾 + 1))) |