Step | Hyp | Ref
| Expression |
1 | | bpolydiflem.1 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | 1 | nnnn0d 11228 |
. . . 4
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
3 | | bpolydiflem.2 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ ℂ) |
4 | | peano2cn 10087 |
. . . . 5
⊢ (𝑋 ∈ ℂ → (𝑋 + 1) ∈
ℂ) |
5 | 3, 4 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑋 + 1) ∈ ℂ) |
6 | | bpolyval 14619 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ (𝑋 + 1) ∈
ℂ) → (𝑁 BernPoly
(𝑋 + 1)) = (((𝑋 + 1)↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1))))) |
7 | 2, 5, 6 | syl2anc 691 |
. . 3
⊢ (𝜑 → (𝑁 BernPoly (𝑋 + 1)) = (((𝑋 + 1)↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1))))) |
8 | | bpolyval 14619 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (𝑁 BernPoly 𝑋) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))))) |
9 | 2, 3, 8 | syl2anc 691 |
. . 3
⊢ (𝜑 → (𝑁 BernPoly 𝑋) = ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))))) |
10 | 7, 9 | oveq12d 6567 |
. 2
⊢ (𝜑 → ((𝑁 BernPoly (𝑋 + 1)) − (𝑁 BernPoly 𝑋)) = ((((𝑋 + 1)↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1)))) − ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))))) |
11 | 5, 2 | expcld 12870 |
. . 3
⊢ (𝜑 → ((𝑋 + 1)↑𝑁) ∈ ℂ) |
12 | | fzfid 12634 |
. . . 4
⊢ (𝜑 → (0...(𝑁 − 1)) ∈ Fin) |
13 | | elfzelz 12213 |
. . . . . . 7
⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℤ) |
14 | | bccl 12971 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ ℤ)
→ (𝑁C𝑘) ∈
ℕ0) |
15 | 2, 13, 14 | syl2an 493 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝑁C𝑘) ∈
ℕ0) |
16 | 15 | nn0cnd 11230 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝑁C𝑘) ∈ ℂ) |
17 | | elfznn0 12302 |
. . . . . . 7
⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ0) |
18 | | bpolycl 14622 |
. . . . . . 7
⊢ ((𝑘 ∈ ℕ0
∧ (𝑋 + 1) ∈
ℂ) → (𝑘 BernPoly
(𝑋 + 1)) ∈
ℂ) |
19 | 17, 5, 18 | syl2anr 494 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝑘 BernPoly (𝑋 + 1)) ∈ ℂ) |
20 | | fzssp1 12255 |
. . . . . . . . . . 11
⊢
(0...(𝑁 − 1))
⊆ (0...((𝑁 − 1)
+ 1)) |
21 | 1 | nncnd 10913 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℂ) |
22 | | ax-1cn 9873 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
23 | | npcan 10169 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 −
1) + 1) = 𝑁) |
24 | 21, 22, 23 | sylancl 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁) |
25 | 24 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝜑 → (0...((𝑁 − 1) + 1)) = (0...𝑁)) |
26 | 20, 25 | syl5sseq 3616 |
. . . . . . . . . 10
⊢ (𝜑 → (0...(𝑁 − 1)) ⊆ (0...𝑁)) |
27 | 26 | sselda 3568 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ (0...𝑁)) |
28 | | fznn0sub 12244 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...𝑁) → (𝑁 − 𝑘) ∈
ℕ0) |
29 | 27, 28 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝑁 − 𝑘) ∈
ℕ0) |
30 | | nn0p1nn 11209 |
. . . . . . . 8
⊢ ((𝑁 − 𝑘) ∈ ℕ0 → ((𝑁 − 𝑘) + 1) ∈ ℕ) |
31 | 29, 30 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑁 − 𝑘) + 1) ∈ ℕ) |
32 | 31 | nncnd 10913 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑁 − 𝑘) + 1) ∈ ℂ) |
33 | 31 | nnne0d 10942 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑁 − 𝑘) + 1) ≠ 0) |
34 | 19, 32, 33 | divcld 10680 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1)) ∈ ℂ) |
35 | 16, 34 | mulcld 9939 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑁C𝑘) · ((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1))) ∈ ℂ) |
36 | 12, 35 | fsumcl 14311 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1))) ∈ ℂ) |
37 | 3, 2 | expcld 12870 |
. . 3
⊢ (𝜑 → (𝑋↑𝑁) ∈ ℂ) |
38 | | bpolycl 14622 |
. . . . . . 7
⊢ ((𝑘 ∈ ℕ0
∧ 𝑋 ∈ ℂ)
→ (𝑘 BernPoly 𝑋) ∈
ℂ) |
39 | 17, 3, 38 | syl2anr 494 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝑘 BernPoly 𝑋) ∈ ℂ) |
40 | 39, 32, 33 | divcld 10680 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)) ∈ ℂ) |
41 | 16, 40 | mulcld 9939 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))) ∈ ℂ) |
42 | 12, 41 | fsumcl 14311 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))) ∈ ℂ) |
43 | 11, 36, 37, 42 | sub4d 10320 |
. 2
⊢ (𝜑 → ((((𝑋 + 1)↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1)))) − ((𝑋↑𝑁) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))))) = ((((𝑋 + 1)↑𝑁) − (𝑋↑𝑁)) − (Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1))) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))))) |
44 | | addcom 10101 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑋 + 1) =
(1 + 𝑋)) |
45 | 3, 22, 44 | sylancl 693 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 + 1) = (1 + 𝑋)) |
46 | 45 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑋 + 1)↑𝑁) = ((1 + 𝑋)↑𝑁)) |
47 | | binom1p 14402 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ ((1 + 𝑋)↑𝑁) = Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (𝑋↑𝑚))) |
48 | 3, 2, 47 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → ((1 + 𝑋)↑𝑁) = Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (𝑋↑𝑚))) |
49 | 46, 48 | eqtrd 2644 |
. . . . . . . 8
⊢ (𝜑 → ((𝑋 + 1)↑𝑁) = Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (𝑋↑𝑚))) |
50 | | nn0uz 11598 |
. . . . . . . . . 10
⊢
ℕ0 = (ℤ≥‘0) |
51 | 2, 50 | syl6eleq 2698 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘0)) |
52 | | bccl2 12972 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ (0...𝑁) → (𝑁C𝑚) ∈ ℕ) |
53 | 52 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℕ) |
54 | 53 | nncnd 10913 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (0...𝑁)) → (𝑁C𝑚) ∈ ℂ) |
55 | | elfznn0 12302 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℕ0) |
56 | | expcl 12740 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ ℂ ∧ 𝑚 ∈ ℕ0)
→ (𝑋↑𝑚) ∈
ℂ) |
57 | 3, 55, 56 | syl2an 493 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (0...𝑁)) → (𝑋↑𝑚) ∈ ℂ) |
58 | 54, 57 | mulcld 9939 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (0...𝑁)) → ((𝑁C𝑚) · (𝑋↑𝑚)) ∈ ℂ) |
59 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑁 → (𝑁C𝑚) = (𝑁C𝑁)) |
60 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑁 → (𝑋↑𝑚) = (𝑋↑𝑁)) |
61 | 59, 60 | oveq12d 6567 |
. . . . . . . . 9
⊢ (𝑚 = 𝑁 → ((𝑁C𝑚) · (𝑋↑𝑚)) = ((𝑁C𝑁) · (𝑋↑𝑁))) |
62 | 51, 58, 61 | fsumm1 14324 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑚 ∈ (0...𝑁)((𝑁C𝑚) · (𝑋↑𝑚)) = (Σ𝑚 ∈ (0...(𝑁 − 1))((𝑁C𝑚) · (𝑋↑𝑚)) + ((𝑁C𝑁) · (𝑋↑𝑁)))) |
63 | | bcnn 12961 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ (𝑁C𝑁) = 1) |
64 | 2, 63 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁C𝑁) = 1) |
65 | 64 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑁C𝑁) · (𝑋↑𝑁)) = (1 · (𝑋↑𝑁))) |
66 | 37 | mulid2d 9937 |
. . . . . . . . . 10
⊢ (𝜑 → (1 · (𝑋↑𝑁)) = (𝑋↑𝑁)) |
67 | 65, 66 | eqtrd 2644 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁C𝑁) · (𝑋↑𝑁)) = (𝑋↑𝑁)) |
68 | 67 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝜑 → (Σ𝑚 ∈ (0...(𝑁 − 1))((𝑁C𝑚) · (𝑋↑𝑚)) + ((𝑁C𝑁) · (𝑋↑𝑁))) = (Σ𝑚 ∈ (0...(𝑁 − 1))((𝑁C𝑚) · (𝑋↑𝑚)) + (𝑋↑𝑁))) |
69 | 49, 62, 68 | 3eqtrd 2648 |
. . . . . . 7
⊢ (𝜑 → ((𝑋 + 1)↑𝑁) = (Σ𝑚 ∈ (0...(𝑁 − 1))((𝑁C𝑚) · (𝑋↑𝑚)) + (𝑋↑𝑁))) |
70 | 69 | oveq1d 6564 |
. . . . . 6
⊢ (𝜑 → (((𝑋 + 1)↑𝑁) − (𝑋↑𝑁)) = ((Σ𝑚 ∈ (0...(𝑁 − 1))((𝑁C𝑚) · (𝑋↑𝑚)) + (𝑋↑𝑁)) − (𝑋↑𝑁))) |
71 | 26 | sselda 3568 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑁 − 1))) → 𝑚 ∈ (0...𝑁)) |
72 | 71, 58 | syldan 486 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑁 − 1))) → ((𝑁C𝑚) · (𝑋↑𝑚)) ∈ ℂ) |
73 | 12, 72 | fsumcl 14311 |
. . . . . . 7
⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑁 − 1))((𝑁C𝑚) · (𝑋↑𝑚)) ∈ ℂ) |
74 | 73, 37 | pncand 10272 |
. . . . . 6
⊢ (𝜑 → ((Σ𝑚 ∈ (0...(𝑁 − 1))((𝑁C𝑚) · (𝑋↑𝑚)) + (𝑋↑𝑁)) − (𝑋↑𝑁)) = Σ𝑚 ∈ (0...(𝑁 − 1))((𝑁C𝑚) · (𝑋↑𝑚))) |
75 | 70, 74 | eqtrd 2644 |
. . . . 5
⊢ (𝜑 → (((𝑋 + 1)↑𝑁) − (𝑋↑𝑁)) = Σ𝑚 ∈ (0...(𝑁 − 1))((𝑁C𝑚) · (𝑋↑𝑚))) |
76 | | nnm1nn0 11211 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
77 | 1, 76 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑁 − 1) ∈
ℕ0) |
78 | 77, 50 | syl6eleq 2698 |
. . . . . 6
⊢ (𝜑 → (𝑁 − 1) ∈
(ℤ≥‘0)) |
79 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑚 = (𝑁 − 1) → (𝑁C𝑚) = (𝑁C(𝑁 − 1))) |
80 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑚 = (𝑁 − 1) → (𝑋↑𝑚) = (𝑋↑(𝑁 − 1))) |
81 | 79, 80 | oveq12d 6567 |
. . . . . 6
⊢ (𝑚 = (𝑁 − 1) → ((𝑁C𝑚) · (𝑋↑𝑚)) = ((𝑁C(𝑁 − 1)) · (𝑋↑(𝑁 − 1)))) |
82 | 78, 72, 81 | fsumm1 14324 |
. . . . 5
⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑁 − 1))((𝑁C𝑚) · (𝑋↑𝑚)) = (Σ𝑚 ∈ (0...((𝑁 − 1) − 1))((𝑁C𝑚) · (𝑋↑𝑚)) + ((𝑁C(𝑁 − 1)) · (𝑋↑(𝑁 − 1))))) |
83 | | 1cnd 9935 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℂ) |
84 | 21, 83, 83 | subsub4d 10302 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁 − 1) − 1) = (𝑁 − (1 + 1))) |
85 | | df-2 10956 |
. . . . . . . . . 10
⊢ 2 = (1 +
1) |
86 | 85 | oveq2i 6560 |
. . . . . . . . 9
⊢ (𝑁 − 2) = (𝑁 − (1 + 1)) |
87 | 84, 86 | syl6eqr 2662 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁 − 1) − 1) = (𝑁 − 2)) |
88 | 87 | oveq2d 6565 |
. . . . . . 7
⊢ (𝜑 → (0...((𝑁 − 1) − 1)) = (0...(𝑁 − 2))) |
89 | 88 | sumeq1d 14279 |
. . . . . 6
⊢ (𝜑 → Σ𝑚 ∈ (0...((𝑁 − 1) − 1))((𝑁C𝑚) · (𝑋↑𝑚)) = Σ𝑚 ∈ (0...(𝑁 − 2))((𝑁C𝑚) · (𝑋↑𝑚))) |
90 | | bcnm1 12976 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (𝑁C(𝑁 − 1)) = 𝑁) |
91 | 2, 90 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑁C(𝑁 − 1)) = 𝑁) |
92 | 91 | oveq1d 6564 |
. . . . . 6
⊢ (𝜑 → ((𝑁C(𝑁 − 1)) · (𝑋↑(𝑁 − 1))) = (𝑁 · (𝑋↑(𝑁 − 1)))) |
93 | 89, 92 | oveq12d 6567 |
. . . . 5
⊢ (𝜑 → (Σ𝑚 ∈ (0...((𝑁 − 1) − 1))((𝑁C𝑚) · (𝑋↑𝑚)) + ((𝑁C(𝑁 − 1)) · (𝑋↑(𝑁 − 1)))) = (Σ𝑚 ∈ (0...(𝑁 − 2))((𝑁C𝑚) · (𝑋↑𝑚)) + (𝑁 · (𝑋↑(𝑁 − 1))))) |
94 | 75, 82, 93 | 3eqtrd 2648 |
. . . 4
⊢ (𝜑 → (((𝑋 + 1)↑𝑁) − (𝑋↑𝑁)) = (Σ𝑚 ∈ (0...(𝑁 − 2))((𝑁C𝑚) · (𝑋↑𝑚)) + (𝑁 · (𝑋↑(𝑁 − 1))))) |
95 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑘 = 0 → (𝑁C𝑘) = (𝑁C0)) |
96 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑘 = 0 → (𝑘 BernPoly (𝑋 + 1)) = (0 BernPoly (𝑋 + 1))) |
97 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑘 = 0 → (𝑁 − 𝑘) = (𝑁 − 0)) |
98 | 97 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝑘 = 0 → ((𝑁 − 𝑘) + 1) = ((𝑁 − 0) + 1)) |
99 | 96, 98 | oveq12d 6567 |
. . . . . . . . 9
⊢ (𝑘 = 0 → ((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1)) = ((0 BernPoly (𝑋 + 1)) / ((𝑁 − 0) + 1))) |
100 | 95, 99 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑘 = 0 → ((𝑁C𝑘) · ((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1))) = ((𝑁C0) · ((0 BernPoly (𝑋 + 1)) / ((𝑁 − 0) + 1)))) |
101 | 78, 35, 100 | fsum1p 14326 |
. . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1))) = (((𝑁C0) · ((0 BernPoly (𝑋 + 1)) / ((𝑁 − 0) + 1))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1))))) |
102 | | bpoly0 14620 |
. . . . . . . . . . 11
⊢ ((𝑋 + 1) ∈ ℂ → (0
BernPoly (𝑋 + 1)) =
1) |
103 | 5, 102 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (0 BernPoly (𝑋 + 1)) = 1) |
104 | 103 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝜑 → ((0 BernPoly (𝑋 + 1)) / ((𝑁 − 0) + 1)) = (1 / ((𝑁 − 0) + 1))) |
105 | 104 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁C0) · ((0 BernPoly (𝑋 + 1)) / ((𝑁 − 0) + 1))) = ((𝑁C0) · (1 / ((𝑁 − 0) + 1)))) |
106 | 105 | oveq1d 6564 |
. . . . . . 7
⊢ (𝜑 → (((𝑁C0) · ((0 BernPoly (𝑋 + 1)) / ((𝑁 − 0) + 1))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1)))) = (((𝑁C0) · (1 / ((𝑁 − 0) + 1))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1))))) |
107 | 101, 106 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1))) = (((𝑁C0) · (1 / ((𝑁 − 0) + 1))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1))))) |
108 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑘 = 0 → (𝑘 BernPoly 𝑋) = (0 BernPoly 𝑋)) |
109 | 108, 98 | oveq12d 6567 |
. . . . . . . . 9
⊢ (𝑘 = 0 → ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)) = ((0 BernPoly 𝑋) / ((𝑁 − 0) + 1))) |
110 | 95, 109 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑘 = 0 → ((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))) = ((𝑁C0) · ((0 BernPoly 𝑋) / ((𝑁 − 0) + 1)))) |
111 | 78, 41, 110 | fsum1p 14326 |
. . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))) = (((𝑁C0) · ((0 BernPoly 𝑋) / ((𝑁 − 0) + 1))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))))) |
112 | | bpoly0 14620 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ ℂ → (0
BernPoly 𝑋) =
1) |
113 | 3, 112 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (0 BernPoly 𝑋) = 1) |
114 | 113 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝜑 → ((0 BernPoly 𝑋) / ((𝑁 − 0) + 1)) = (1 / ((𝑁 − 0) + 1))) |
115 | 114 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁C0) · ((0 BernPoly 𝑋) / ((𝑁 − 0) + 1))) = ((𝑁C0) · (1 / ((𝑁 − 0) + 1)))) |
116 | 115 | oveq1d 6564 |
. . . . . . 7
⊢ (𝜑 → (((𝑁C0) · ((0 BernPoly 𝑋) / ((𝑁 − 0) + 1))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))) = (((𝑁C0) · (1 / ((𝑁 − 0) + 1))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))))) |
117 | 111, 116 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))) = (((𝑁C0) · (1 / ((𝑁 − 0) + 1))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))))) |
118 | 107, 117 | oveq12d 6567 |
. . . . 5
⊢ (𝜑 → (Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1))) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))) = ((((𝑁C0) · (1 / ((𝑁 − 0) + 1))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1)))) − (((𝑁C0) · (1 / ((𝑁 − 0) + 1))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))))) |
119 | | 0z 11265 |
. . . . . . . . 9
⊢ 0 ∈
ℤ |
120 | | bccl 12971 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 0 ∈ ℤ) → (𝑁C0) ∈
ℕ0) |
121 | 2, 119, 120 | sylancl 693 |
. . . . . . . 8
⊢ (𝜑 → (𝑁C0) ∈
ℕ0) |
122 | 121 | nn0cnd 11230 |
. . . . . . 7
⊢ (𝜑 → (𝑁C0) ∈ ℂ) |
123 | 21 | subid1d 10260 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 − 0) = 𝑁) |
124 | 123, 1 | eqeltrd 2688 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 − 0) ∈ ℕ) |
125 | 124 | peano2nnd 10914 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑁 − 0) + 1) ∈
ℕ) |
126 | 125 | nnrecred 10943 |
. . . . . . . 8
⊢ (𝜑 → (1 / ((𝑁 − 0) + 1)) ∈
ℝ) |
127 | 126 | recnd 9947 |
. . . . . . 7
⊢ (𝜑 → (1 / ((𝑁 − 0) + 1)) ∈
ℂ) |
128 | 122, 127 | mulcld 9939 |
. . . . . 6
⊢ (𝜑 → ((𝑁C0) · (1 / ((𝑁 − 0) + 1))) ∈
ℂ) |
129 | | fzfid 12634 |
. . . . . . 7
⊢ (𝜑 → ((0 + 1)...(𝑁 − 1)) ∈
Fin) |
130 | | fzp1ss 12262 |
. . . . . . . . . 10
⊢ (0 ∈
ℤ → ((0 + 1)...(𝑁 − 1)) ⊆ (0...(𝑁 − 1))) |
131 | 119, 130 | ax-mp 5 |
. . . . . . . . 9
⊢ ((0 +
1)...(𝑁 − 1)) ⊆
(0...(𝑁 −
1)) |
132 | 131 | sseli 3564 |
. . . . . . . 8
⊢ (𝑘 ∈ ((0 + 1)...(𝑁 − 1)) → 𝑘 ∈ (0...(𝑁 − 1))) |
133 | 132, 35 | sylan2 490 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 − 1))) → ((𝑁C𝑘) · ((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1))) ∈ ℂ) |
134 | 129, 133 | fsumcl 14311 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1))) ∈ ℂ) |
135 | 132, 41 | sylan2 490 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 − 1))) → ((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))) ∈ ℂ) |
136 | 129, 135 | fsumcl 14311 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))) ∈ ℂ) |
137 | 128, 134,
136 | pnpcand 10308 |
. . . . 5
⊢ (𝜑 → ((((𝑁C0) · (1 / ((𝑁 − 0) + 1))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1)))) − (((𝑁C0) · (1 / ((𝑁 − 0) + 1))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))))) = (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1))) − Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))))) |
138 | | 1zzd 11285 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℤ) |
139 | | 0zd 11266 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
ℤ) |
140 | 1 | nnzd 11357 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℤ) |
141 | | 2z 11286 |
. . . . . . . . 9
⊢ 2 ∈
ℤ |
142 | | zsubcl 11296 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 2 ∈
ℤ) → (𝑁 −
2) ∈ ℤ) |
143 | 140, 141,
142 | sylancl 693 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 − 2) ∈ ℤ) |
144 | | fzssp1 12255 |
. . . . . . . . . . 11
⊢
(0...(𝑁 − 2))
⊆ (0...((𝑁 − 2)
+ 1)) |
145 | | 2m1e1 11012 |
. . . . . . . . . . . . . 14
⊢ (2
− 1) = 1 |
146 | 145 | oveq2i 6560 |
. . . . . . . . . . . . 13
⊢ (𝑁 − (2 − 1)) = (𝑁 − 1) |
147 | | 2cnd 10970 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 2 ∈
ℂ) |
148 | 21, 147, 83 | subsubd 10299 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 − (2 − 1)) = ((𝑁 − 2) +
1)) |
149 | 146, 148 | syl5reqr 2659 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑁 − 2) + 1) = (𝑁 − 1)) |
150 | 149 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝜑 → (0...((𝑁 − 2) + 1)) = (0...(𝑁 − 1))) |
151 | 144, 150 | syl5sseq 3616 |
. . . . . . . . . 10
⊢ (𝜑 → (0...(𝑁 − 2)) ⊆ (0...(𝑁 − 1))) |
152 | 151 | sselda 3568 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑁 − 2))) → 𝑚 ∈ (0...(𝑁 − 1))) |
153 | 152, 72 | syldan 486 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑁 − 2))) → ((𝑁C𝑚) · (𝑋↑𝑚)) ∈ ℂ) |
154 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑚 = (𝑘 − 1) → (𝑁C𝑚) = (𝑁C(𝑘 − 1))) |
155 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑚 = (𝑘 − 1) → (𝑋↑𝑚) = (𝑋↑(𝑘 − 1))) |
156 | 154, 155 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑚 = (𝑘 − 1) → ((𝑁C𝑚) · (𝑋↑𝑚)) = ((𝑁C(𝑘 − 1)) · (𝑋↑(𝑘 − 1)))) |
157 | 138, 139,
143, 153, 156 | fsumshft 14354 |
. . . . . . 7
⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑁 − 2))((𝑁C𝑚) · (𝑋↑𝑚)) = Σ𝑘 ∈ ((0 + 1)...((𝑁 − 2) + 1))((𝑁C(𝑘 − 1)) · (𝑋↑(𝑘 − 1)))) |
158 | 149 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝜑 → ((0 + 1)...((𝑁 − 2) + 1)) = ((0 +
1)...(𝑁 −
1))) |
159 | 158 | sumeq1d 14279 |
. . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...((𝑁 − 2) + 1))((𝑁C(𝑘 − 1)) · (𝑋↑(𝑘 − 1))) = Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝑁C(𝑘 − 1)) · (𝑋↑(𝑘 − 1)))) |
160 | 157, 159 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑁 − 2))((𝑁C𝑚) · (𝑋↑𝑚)) = Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝑁C(𝑘 − 1)) · (𝑋↑(𝑘 − 1)))) |
161 | | 0p1e1 11009 |
. . . . . . . . . 10
⊢ (0 + 1) =
1 |
162 | 161 | oveq1i 6559 |
. . . . . . . . 9
⊢ ((0 +
1)...(𝑁 − 1)) =
(1...(𝑁 −
1)) |
163 | 162 | eleq2i 2680 |
. . . . . . . 8
⊢ (𝑘 ∈ ((0 + 1)...(𝑁 − 1)) ↔ 𝑘 ∈ (1...(𝑁 − 1))) |
164 | | fzssp1 12255 |
. . . . . . . . . . . . . 14
⊢
(1...(𝑁 − 1))
⊆ (1...((𝑁 − 1)
+ 1)) |
165 | 24 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁)) |
166 | 164, 165 | syl5sseq 3616 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁)) |
167 | 166 | sselda 3568 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → 𝑘 ∈ (1...𝑁)) |
168 | | bcm1k 12964 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...𝑁) → (𝑁C𝑘) = ((𝑁C(𝑘 − 1)) · ((𝑁 − (𝑘 − 1)) / 𝑘))) |
169 | 167, 168 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (𝑁C𝑘) = ((𝑁C(𝑘 − 1)) · ((𝑁 − (𝑘 − 1)) / 𝑘))) |
170 | 1 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → 𝑁 ∈ ℕ) |
171 | 170 | nncnd 10913 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → 𝑁 ∈ ℂ) |
172 | | elfznn 12241 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (1...(𝑁 − 1)) → 𝑘 ∈ ℕ) |
173 | 172 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → 𝑘 ∈ ℕ) |
174 | 173 | nncnd 10913 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → 𝑘 ∈ ℂ) |
175 | | 1cnd 9935 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → 1 ∈
ℂ) |
176 | 171, 174,
175 | subsubd 10299 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (𝑁 − (𝑘 − 1)) = ((𝑁 − 𝑘) + 1)) |
177 | 176 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → ((𝑁 − (𝑘 − 1)) / 𝑘) = (((𝑁 − 𝑘) + 1) / 𝑘)) |
178 | 177 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → ((𝑁C(𝑘 − 1)) · ((𝑁 − (𝑘 − 1)) / 𝑘)) = ((𝑁C(𝑘 − 1)) · (((𝑁 − 𝑘) + 1) / 𝑘))) |
179 | 169, 178 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (𝑁C𝑘) = ((𝑁C(𝑘 − 1)) · (((𝑁 − 𝑘) + 1) / 𝑘))) |
180 | | bpolydiflem.3 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → ((𝑘 BernPoly (𝑋 + 1)) − (𝑘 BernPoly 𝑋)) = (𝑘 · (𝑋↑(𝑘 − 1)))) |
181 | 180 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (((𝑘 BernPoly (𝑋 + 1)) − (𝑘 BernPoly 𝑋)) / ((𝑁 − 𝑘) + 1)) = ((𝑘 · (𝑋↑(𝑘 − 1))) / ((𝑁 − 𝑘) + 1))) |
182 | 163, 132 | sylbir 224 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1...(𝑁 − 1)) → 𝑘 ∈ (0...(𝑁 − 1))) |
183 | 182, 19 | sylan2 490 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (𝑘 BernPoly (𝑋 + 1)) ∈ ℂ) |
184 | 182, 39 | sylan2 490 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (𝑘 BernPoly 𝑋) ∈ ℂ) |
185 | 182, 32 | sylan2 490 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → ((𝑁 − 𝑘) + 1) ∈ ℂ) |
186 | 182, 33 | sylan2 490 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → ((𝑁 − 𝑘) + 1) ≠ 0) |
187 | 183, 184,
185, 186 | divsubdird 10719 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (((𝑘 BernPoly (𝑋 + 1)) − (𝑘 BernPoly 𝑋)) / ((𝑁 − 𝑘) + 1)) = (((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1)) − ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))) |
188 | 3 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → 𝑋 ∈ ℂ) |
189 | | nnm1nn0 11211 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → (𝑘 − 1) ∈
ℕ0) |
190 | 173, 189 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (𝑘 − 1) ∈
ℕ0) |
191 | 188, 190 | expcld 12870 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (𝑋↑(𝑘 − 1)) ∈ ℂ) |
192 | 174, 191,
185, 186 | div23d 10717 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → ((𝑘 · (𝑋↑(𝑘 − 1))) / ((𝑁 − 𝑘) + 1)) = ((𝑘 / ((𝑁 − 𝑘) + 1)) · (𝑋↑(𝑘 − 1)))) |
193 | 181, 187,
192 | 3eqtr3d 2652 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1)) − ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))) = ((𝑘 / ((𝑁 − 𝑘) + 1)) · (𝑋↑(𝑘 − 1)))) |
194 | 179, 193 | oveq12d 6567 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → ((𝑁C𝑘) · (((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1)) − ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))) = (((𝑁C(𝑘 − 1)) · (((𝑁 − 𝑘) + 1) / 𝑘)) · ((𝑘 / ((𝑁 − 𝑘) + 1)) · (𝑋↑(𝑘 − 1))))) |
195 | 182, 16 | sylan2 490 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (𝑁C𝑘) ∈ ℂ) |
196 | 183, 185,
186 | divcld 10680 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → ((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1)) ∈ ℂ) |
197 | 184, 185,
186 | divcld 10680 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)) ∈ ℂ) |
198 | 195, 196,
197 | subdid 10365 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → ((𝑁C𝑘) · (((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1)) − ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))) = (((𝑁C𝑘) · ((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1))) − ((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))))) |
199 | 170 | nnnn0d 11228 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → 𝑁 ∈
ℕ0) |
200 | 190 | nn0zd 11356 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (𝑘 − 1) ∈ ℤ) |
201 | | bccl 12971 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ (𝑘 − 1) ∈
ℤ) → (𝑁C(𝑘 − 1)) ∈
ℕ0) |
202 | 199, 200,
201 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (𝑁C(𝑘 − 1)) ∈
ℕ0) |
203 | 202 | nn0cnd 11230 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (𝑁C(𝑘 − 1)) ∈ ℂ) |
204 | 173 | nnne0d 10942 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → 𝑘 ≠ 0) |
205 | 185, 174,
204 | divcld 10680 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (((𝑁 − 𝑘) + 1) / 𝑘) ∈ ℂ) |
206 | 174, 185,
186 | divcld 10680 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (𝑘 / ((𝑁 − 𝑘) + 1)) ∈ ℂ) |
207 | 206, 191 | mulcld 9939 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → ((𝑘 / ((𝑁 − 𝑘) + 1)) · (𝑋↑(𝑘 − 1))) ∈
ℂ) |
208 | 203, 205,
207 | mulassd 9942 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (((𝑁C(𝑘 − 1)) · (((𝑁 − 𝑘) + 1) / 𝑘)) · ((𝑘 / ((𝑁 − 𝑘) + 1)) · (𝑋↑(𝑘 − 1)))) = ((𝑁C(𝑘 − 1)) · ((((𝑁 − 𝑘) + 1) / 𝑘) · ((𝑘 / ((𝑁 − 𝑘) + 1)) · (𝑋↑(𝑘 − 1)))))) |
209 | 185, 174,
186, 204 | divcan6d 10699 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → ((((𝑁 − 𝑘) + 1) / 𝑘) · (𝑘 / ((𝑁 − 𝑘) + 1))) = 1) |
210 | 209 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (((((𝑁 − 𝑘) + 1) / 𝑘) · (𝑘 / ((𝑁 − 𝑘) + 1))) · (𝑋↑(𝑘 − 1))) = (1 · (𝑋↑(𝑘 − 1)))) |
211 | 205, 206,
191 | mulassd 9942 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (((((𝑁 − 𝑘) + 1) / 𝑘) · (𝑘 / ((𝑁 − 𝑘) + 1))) · (𝑋↑(𝑘 − 1))) = ((((𝑁 − 𝑘) + 1) / 𝑘) · ((𝑘 / ((𝑁 − 𝑘) + 1)) · (𝑋↑(𝑘 − 1))))) |
212 | 191 | mulid2d 9937 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (1 · (𝑋↑(𝑘 − 1))) = (𝑋↑(𝑘 − 1))) |
213 | 210, 211,
212 | 3eqtr3d 2652 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → ((((𝑁 − 𝑘) + 1) / 𝑘) · ((𝑘 / ((𝑁 − 𝑘) + 1)) · (𝑋↑(𝑘 − 1)))) = (𝑋↑(𝑘 − 1))) |
214 | 213 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → ((𝑁C(𝑘 − 1)) · ((((𝑁 − 𝑘) + 1) / 𝑘) · ((𝑘 / ((𝑁 − 𝑘) + 1)) · (𝑋↑(𝑘 − 1))))) = ((𝑁C(𝑘 − 1)) · (𝑋↑(𝑘 − 1)))) |
215 | 208, 214 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (((𝑁C(𝑘 − 1)) · (((𝑁 − 𝑘) + 1) / 𝑘)) · ((𝑘 / ((𝑁 − 𝑘) + 1)) · (𝑋↑(𝑘 − 1)))) = ((𝑁C(𝑘 − 1)) · (𝑋↑(𝑘 − 1)))) |
216 | 194, 198,
215 | 3eqtr3d 2652 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (((𝑁C𝑘) · ((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1))) − ((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))) = ((𝑁C(𝑘 − 1)) · (𝑋↑(𝑘 − 1)))) |
217 | 163, 216 | sylan2b 491 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 − 1))) → (((𝑁C𝑘) · ((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1))) − ((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))) = ((𝑁C(𝑘 − 1)) · (𝑋↑(𝑘 − 1)))) |
218 | 217 | sumeq2dv 14281 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(((𝑁C𝑘) · ((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1))) − ((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))) = Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝑁C(𝑘 − 1)) · (𝑋↑(𝑘 − 1)))) |
219 | 129, 133,
135 | fsumsub 14362 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))(((𝑁C𝑘) · ((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1))) − ((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))) = (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1))) − Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))))) |
220 | 160, 218,
219 | 3eqtr2rd 2651 |
. . . . 5
⊢ (𝜑 → (Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1))) − Σ𝑘 ∈ ((0 + 1)...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))) = Σ𝑚 ∈ (0...(𝑁 − 2))((𝑁C𝑚) · (𝑋↑𝑚))) |
221 | 118, 137,
220 | 3eqtrd 2648 |
. . . 4
⊢ (𝜑 → (Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1))) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1)))) = Σ𝑚 ∈ (0...(𝑁 − 2))((𝑁C𝑚) · (𝑋↑𝑚))) |
222 | 94, 221 | oveq12d 6567 |
. . 3
⊢ (𝜑 → ((((𝑋 + 1)↑𝑁) − (𝑋↑𝑁)) − (Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1))) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))))) = ((Σ𝑚 ∈ (0...(𝑁 − 2))((𝑁C𝑚) · (𝑋↑𝑚)) + (𝑁 · (𝑋↑(𝑁 − 1)))) − Σ𝑚 ∈ (0...(𝑁 − 2))((𝑁C𝑚) · (𝑋↑𝑚)))) |
223 | | fzfid 12634 |
. . . . 5
⊢ (𝜑 → (0...(𝑁 − 2)) ∈ Fin) |
224 | 223, 153 | fsumcl 14311 |
. . . 4
⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑁 − 2))((𝑁C𝑚) · (𝑋↑𝑚)) ∈ ℂ) |
225 | 3, 77 | expcld 12870 |
. . . . 5
⊢ (𝜑 → (𝑋↑(𝑁 − 1)) ∈
ℂ) |
226 | 21, 225 | mulcld 9939 |
. . . 4
⊢ (𝜑 → (𝑁 · (𝑋↑(𝑁 − 1))) ∈
ℂ) |
227 | 224, 226 | pncan2d 10273 |
. . 3
⊢ (𝜑 → ((Σ𝑚 ∈ (0...(𝑁 − 2))((𝑁C𝑚) · (𝑋↑𝑚)) + (𝑁 · (𝑋↑(𝑁 − 1)))) − Σ𝑚 ∈ (0...(𝑁 − 2))((𝑁C𝑚) · (𝑋↑𝑚))) = (𝑁 · (𝑋↑(𝑁 − 1)))) |
228 | 222, 227 | eqtrd 2644 |
. 2
⊢ (𝜑 → ((((𝑋 + 1)↑𝑁) − (𝑋↑𝑁)) − (Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly (𝑋 + 1)) / ((𝑁 − 𝑘) + 1))) − Σ𝑘 ∈ (0...(𝑁 − 1))((𝑁C𝑘) · ((𝑘 BernPoly 𝑋) / ((𝑁 − 𝑘) + 1))))) = (𝑁 · (𝑋↑(𝑁 − 1)))) |
229 | 10, 43, 228 | 3eqtrd 2648 |
1
⊢ (𝜑 → ((𝑁 BernPoly (𝑋 + 1)) − (𝑁 BernPoly 𝑋)) = (𝑁 · (𝑋↑(𝑁 − 1)))) |