Step | Hyp | Ref
| Expression |
1 | | nn0p1nn 11332 |
. . . 4
⊢ (𝐾 ∈ ℕ0
→ (𝐾 + 1) ∈
ℕ) |
2 | 1 | adantr 481 |
. . 3
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝐾 + 1) ∈ ℕ) |
3 | 2 | nncnd 11036 |
. 2
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝐾 + 1) ∈ ℂ) |
4 | | fzfid 12772 |
. . 3
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (0...𝑀) ∈ Fin) |
5 | | elfzelz 12342 |
. . . . 5
⊢ (𝑛 ∈ (0...𝑀) → 𝑛 ∈ ℤ) |
6 | 5 | zcnd 11483 |
. . . 4
⊢ (𝑛 ∈ (0...𝑀) → 𝑛 ∈ ℂ) |
7 | | simpl 473 |
. . . 4
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → 𝐾 ∈
ℕ0) |
8 | | expcl 12878 |
. . . 4
⊢ ((𝑛 ∈ ℂ ∧ 𝐾 ∈ ℕ0)
→ (𝑛↑𝐾) ∈
ℂ) |
9 | 6, 7, 8 | syl2anr 495 |
. . 3
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑛 ∈ (0...𝑀)) → (𝑛↑𝐾) ∈ ℂ) |
10 | 4, 9 | fsumcl 14464 |
. 2
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → Σ𝑛 ∈ (0...𝑀)(𝑛↑𝐾) ∈ ℂ) |
11 | 2 | nnne0d 11065 |
. 2
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝐾 + 1) ≠ 0) |
12 | 4, 3, 9 | fsummulc2 14516 |
. . 3
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → ((𝐾 + 1) · Σ𝑛 ∈ (0...𝑀)(𝑛↑𝐾)) = Σ𝑛 ∈ (0...𝑀)((𝐾 + 1) · (𝑛↑𝐾))) |
13 | | bpolydif 14786 |
. . . . . 6
⊢ (((𝐾 + 1) ∈ ℕ ∧ 𝑛 ∈ ℂ) → (((𝐾 + 1) BernPoly (𝑛 + 1)) − ((𝐾 + 1) BernPoly 𝑛)) = ((𝐾 + 1) · (𝑛↑((𝐾 + 1) − 1)))) |
14 | 2, 6, 13 | syl2an 494 |
. . . . 5
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑛 ∈ (0...𝑀)) → (((𝐾 + 1) BernPoly (𝑛 + 1)) − ((𝐾 + 1) BernPoly 𝑛)) = ((𝐾 + 1) · (𝑛↑((𝐾 + 1) − 1)))) |
15 | | nn0cn 11302 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℂ) |
16 | 15 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑛 ∈ (0...𝑀)) → 𝐾 ∈ ℂ) |
17 | | ax-1cn 9994 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
18 | | pncan 10287 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐾 + 1)
− 1) = 𝐾) |
19 | 16, 17, 18 | sylancl 694 |
. . . . . . 7
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑛 ∈ (0...𝑀)) → ((𝐾 + 1) − 1) = 𝐾) |
20 | 19 | oveq2d 6666 |
. . . . . 6
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑛 ∈ (0...𝑀)) → (𝑛↑((𝐾 + 1) − 1)) = (𝑛↑𝐾)) |
21 | 20 | oveq2d 6666 |
. . . . 5
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑛 ∈ (0...𝑀)) → ((𝐾 + 1) · (𝑛↑((𝐾 + 1) − 1))) = ((𝐾 + 1) · (𝑛↑𝐾))) |
22 | 14, 21 | eqtrd 2656 |
. . . 4
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑛 ∈ (0...𝑀)) → (((𝐾 + 1) BernPoly (𝑛 + 1)) − ((𝐾 + 1) BernPoly 𝑛)) = ((𝐾 + 1) · (𝑛↑𝐾))) |
23 | 22 | sumeq2dv 14433 |
. . 3
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → Σ𝑛 ∈ (0...𝑀)(((𝐾 + 1) BernPoly (𝑛 + 1)) − ((𝐾 + 1) BernPoly 𝑛)) = Σ𝑛 ∈ (0...𝑀)((𝐾 + 1) · (𝑛↑𝐾))) |
24 | | oveq2 6658 |
. . . 4
⊢ (𝑘 = 𝑛 → ((𝐾 + 1) BernPoly 𝑘) = ((𝐾 + 1) BernPoly 𝑛)) |
25 | | oveq2 6658 |
. . . 4
⊢ (𝑘 = (𝑛 + 1) → ((𝐾 + 1) BernPoly 𝑘) = ((𝐾 + 1) BernPoly (𝑛 + 1))) |
26 | | oveq2 6658 |
. . . 4
⊢ (𝑘 = 0 → ((𝐾 + 1) BernPoly 𝑘) = ((𝐾 + 1) BernPoly 0)) |
27 | | oveq2 6658 |
. . . 4
⊢ (𝑘 = (𝑀 + 1) → ((𝐾 + 1) BernPoly 𝑘) = ((𝐾 + 1) BernPoly (𝑀 + 1))) |
28 | | nn0z 11400 |
. . . . 5
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℤ) |
29 | 28 | adantl 482 |
. . . 4
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → 𝑀 ∈ ℤ) |
30 | | peano2nn0 11333 |
. . . . . 6
⊢ (𝑀 ∈ ℕ0
→ (𝑀 + 1) ∈
ℕ0) |
31 | 30 | adantl 482 |
. . . . 5
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝑀 + 1) ∈
ℕ0) |
32 | | nn0uz 11722 |
. . . . 5
⊢
ℕ0 = (ℤ≥‘0) |
33 | 31, 32 | syl6eleq 2711 |
. . . 4
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝑀 + 1) ∈
(ℤ≥‘0)) |
34 | | peano2nn0 11333 |
. . . . . 6
⊢ (𝐾 ∈ ℕ0
→ (𝐾 + 1) ∈
ℕ0) |
35 | 34 | ad2antrr 762 |
. . . . 5
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑘 ∈ (0...(𝑀 + 1))) → (𝐾 + 1) ∈
ℕ0) |
36 | | elfznn0 12433 |
. . . . . . 7
⊢ (𝑘 ∈ (0...(𝑀 + 1)) → 𝑘 ∈ ℕ0) |
37 | 36 | adantl 482 |
. . . . . 6
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑘 ∈ (0...(𝑀 + 1))) → 𝑘 ∈ ℕ0) |
38 | 37 | nn0cnd 11353 |
. . . . 5
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑘 ∈ (0...(𝑀 + 1))) → 𝑘 ∈ ℂ) |
39 | | bpolycl 14783 |
. . . . 5
⊢ (((𝐾 + 1) ∈ ℕ0
∧ 𝑘 ∈ ℂ)
→ ((𝐾 + 1) BernPoly
𝑘) ∈
ℂ) |
40 | 35, 38, 39 | syl2anc 693 |
. . . 4
⊢ (((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ 𝑘 ∈ (0...(𝑀 + 1))) → ((𝐾 + 1) BernPoly 𝑘) ∈ ℂ) |
41 | 24, 25, 26, 27, 29, 33, 40 | telfsum2 14537 |
. . 3
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → Σ𝑛 ∈ (0...𝑀)(((𝐾 + 1) BernPoly (𝑛 + 1)) − ((𝐾 + 1) BernPoly 𝑛)) = (((𝐾 + 1) BernPoly (𝑀 + 1)) − ((𝐾 + 1) BernPoly 0))) |
42 | 12, 23, 41 | 3eqtr2d 2662 |
. 2
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → ((𝐾 + 1) · Σ𝑛 ∈ (0...𝑀)(𝑛↑𝐾)) = (((𝐾 + 1) BernPoly (𝑀 + 1)) − ((𝐾 + 1) BernPoly 0))) |
43 | 3, 10, 11, 42 | mvllmuld 10857 |
1
⊢ ((𝐾 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → Σ𝑛 ∈ (0...𝑀)(𝑛↑𝐾) = ((((𝐾 + 1) BernPoly (𝑀 + 1)) − ((𝐾 + 1) BernPoly 0)) / (𝐾 + 1))) |