| Step |
Hyp |
Ref |
Expression |
| 1 |
|
bpolydiflem.1 |
⊢ ( 𝜑 → 𝑁 ∈ ℕ ) |
| 2 |
|
bpolydiflem.2 |
⊢ ( 𝜑 → 𝑋 ∈ ℂ ) |
| 3 |
|
bpolydiflem.3 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) − ( 𝑘 BernPoly 𝑋 ) ) = ( 𝑘 · ( 𝑋 ↑ ( 𝑘 − 1 ) ) ) ) |
| 4 |
1
|
nnnn0d |
⊢ ( 𝜑 → 𝑁 ∈ ℕ0 ) |
| 5 |
|
peano2cn |
⊢ ( 𝑋 ∈ ℂ → ( 𝑋 + 1 ) ∈ ℂ ) |
| 6 |
2 5
|
syl |
⊢ ( 𝜑 → ( 𝑋 + 1 ) ∈ ℂ ) |
| 7 |
|
bpolyval |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑋 + 1 ) ∈ ℂ ) → ( 𝑁 BernPoly ( 𝑋 + 1 ) ) = ( ( ( 𝑋 + 1 ) ↑ 𝑁 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) ) |
| 8 |
4 6 7
|
syl2anc |
⊢ ( 𝜑 → ( 𝑁 BernPoly ( 𝑋 + 1 ) ) = ( ( ( 𝑋 + 1 ) ↑ 𝑁 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) ) |
| 9 |
|
bpolyval |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( 𝑁 BernPoly 𝑋 ) = ( ( 𝑋 ↑ 𝑁 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) ) |
| 10 |
4 2 9
|
syl2anc |
⊢ ( 𝜑 → ( 𝑁 BernPoly 𝑋 ) = ( ( 𝑋 ↑ 𝑁 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) ) |
| 11 |
8 10
|
oveq12d |
⊢ ( 𝜑 → ( ( 𝑁 BernPoly ( 𝑋 + 1 ) ) − ( 𝑁 BernPoly 𝑋 ) ) = ( ( ( ( 𝑋 + 1 ) ↑ 𝑁 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) − ( ( 𝑋 ↑ 𝑁 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) ) ) |
| 12 |
6 4
|
expcld |
⊢ ( 𝜑 → ( ( 𝑋 + 1 ) ↑ 𝑁 ) ∈ ℂ ) |
| 13 |
|
fzfid |
⊢ ( 𝜑 → ( 0 ... ( 𝑁 − 1 ) ) ∈ Fin ) |
| 14 |
|
elfzelz |
⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ℤ ) |
| 15 |
|
bccl |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℤ ) → ( 𝑁 C 𝑘 ) ∈ ℕ0 ) |
| 16 |
4 14 15
|
syl2an |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑁 C 𝑘 ) ∈ ℕ0 ) |
| 17 |
16
|
nn0cnd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑁 C 𝑘 ) ∈ ℂ ) |
| 18 |
|
elfznn0 |
⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ℕ0 ) |
| 19 |
|
bpolycl |
⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( 𝑋 + 1 ) ∈ ℂ ) → ( 𝑘 BernPoly ( 𝑋 + 1 ) ) ∈ ℂ ) |
| 20 |
18 6 19
|
syl2anr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑘 BernPoly ( 𝑋 + 1 ) ) ∈ ℂ ) |
| 21 |
|
fzssp1 |
⊢ ( 0 ... ( 𝑁 − 1 ) ) ⊆ ( 0 ... ( ( 𝑁 − 1 ) + 1 ) ) |
| 22 |
1
|
nncnd |
⊢ ( 𝜑 → 𝑁 ∈ ℂ ) |
| 23 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
| 24 |
|
npcan |
⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 ) |
| 25 |
22 23 24
|
sylancl |
⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 ) |
| 26 |
25
|
oveq2d |
⊢ ( 𝜑 → ( 0 ... ( ( 𝑁 − 1 ) + 1 ) ) = ( 0 ... 𝑁 ) ) |
| 27 |
21 26
|
sseqtrid |
⊢ ( 𝜑 → ( 0 ... ( 𝑁 − 1 ) ) ⊆ ( 0 ... 𝑁 ) ) |
| 28 |
27
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ( 0 ... 𝑁 ) ) |
| 29 |
|
fznn0sub |
⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( 𝑁 − 𝑘 ) ∈ ℕ0 ) |
| 30 |
28 29
|
syl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑁 − 𝑘 ) ∈ ℕ0 ) |
| 31 |
|
nn0p1nn |
⊢ ( ( 𝑁 − 𝑘 ) ∈ ℕ0 → ( ( 𝑁 − 𝑘 ) + 1 ) ∈ ℕ ) |
| 32 |
30 31
|
syl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 − 𝑘 ) + 1 ) ∈ ℕ ) |
| 33 |
32
|
nncnd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 − 𝑘 ) + 1 ) ∈ ℂ ) |
| 34 |
32
|
nnne0d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 − 𝑘 ) + 1 ) ≠ 0 ) |
| 35 |
20 33 34
|
divcld |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ∈ ℂ ) |
| 36 |
17 35
|
mulcld |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ∈ ℂ ) |
| 37 |
13 36
|
fsumcl |
⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ∈ ℂ ) |
| 38 |
2 4
|
expcld |
⊢ ( 𝜑 → ( 𝑋 ↑ 𝑁 ) ∈ ℂ ) |
| 39 |
|
bpolycl |
⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑋 ∈ ℂ ) → ( 𝑘 BernPoly 𝑋 ) ∈ ℂ ) |
| 40 |
18 2 39
|
syl2anr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑘 BernPoly 𝑋 ) ∈ ℂ ) |
| 41 |
40 33 34
|
divcld |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ∈ ℂ ) |
| 42 |
17 41
|
mulcld |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ∈ ℂ ) |
| 43 |
13 42
|
fsumcl |
⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ∈ ℂ ) |
| 44 |
12 37 38 43
|
sub4d |
⊢ ( 𝜑 → ( ( ( ( 𝑋 + 1 ) ↑ 𝑁 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) − ( ( 𝑋 ↑ 𝑁 ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) ) = ( ( ( ( 𝑋 + 1 ) ↑ 𝑁 ) − ( 𝑋 ↑ 𝑁 ) ) − ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) ) ) |
| 45 |
27
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑚 ∈ ( 0 ... 𝑁 ) ) |
| 46 |
|
bccl2 |
⊢ ( 𝑚 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝑚 ) ∈ ℕ ) |
| 47 |
46
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝑚 ) ∈ ℕ ) |
| 48 |
47
|
nncnd |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝑚 ) ∈ ℂ ) |
| 49 |
|
elfznn0 |
⊢ ( 𝑚 ∈ ( 0 ... 𝑁 ) → 𝑚 ∈ ℕ0 ) |
| 50 |
|
expcl |
⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑚 ∈ ℕ0 ) → ( 𝑋 ↑ 𝑚 ) ∈ ℂ ) |
| 51 |
2 49 50
|
syl2an |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( 𝑋 ↑ 𝑚 ) ∈ ℂ ) |
| 52 |
48 51
|
mulcld |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 C 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ∈ ℂ ) |
| 53 |
45 52
|
syldan |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 C 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ∈ ℂ ) |
| 54 |
13 53
|
fsumcl |
⊢ ( 𝜑 → Σ 𝑚 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ∈ ℂ ) |
| 55 |
|
addcom |
⊢ ( ( 𝑋 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑋 + 1 ) = ( 1 + 𝑋 ) ) |
| 56 |
2 23 55
|
sylancl |
⊢ ( 𝜑 → ( 𝑋 + 1 ) = ( 1 + 𝑋 ) ) |
| 57 |
56
|
oveq1d |
⊢ ( 𝜑 → ( ( 𝑋 + 1 ) ↑ 𝑁 ) = ( ( 1 + 𝑋 ) ↑ 𝑁 ) ) |
| 58 |
|
binom1p |
⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( 1 + 𝑋 ) ↑ 𝑁 ) = Σ 𝑚 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ) |
| 59 |
2 4 58
|
syl2anc |
⊢ ( 𝜑 → ( ( 1 + 𝑋 ) ↑ 𝑁 ) = Σ 𝑚 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ) |
| 60 |
57 59
|
eqtrd |
⊢ ( 𝜑 → ( ( 𝑋 + 1 ) ↑ 𝑁 ) = Σ 𝑚 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ) |
| 61 |
|
nn0uz |
⊢ ℕ0 = ( ℤ≥ ‘ 0 ) |
| 62 |
4 61
|
eleqtrdi |
⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) ) |
| 63 |
|
oveq2 |
⊢ ( 𝑚 = 𝑁 → ( 𝑁 C 𝑚 ) = ( 𝑁 C 𝑁 ) ) |
| 64 |
|
oveq2 |
⊢ ( 𝑚 = 𝑁 → ( 𝑋 ↑ 𝑚 ) = ( 𝑋 ↑ 𝑁 ) ) |
| 65 |
63 64
|
oveq12d |
⊢ ( 𝑚 = 𝑁 → ( ( 𝑁 C 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) = ( ( 𝑁 C 𝑁 ) · ( 𝑋 ↑ 𝑁 ) ) ) |
| 66 |
62 52 65
|
fsumm1 |
⊢ ( 𝜑 → Σ 𝑚 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) = ( Σ 𝑚 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) + ( ( 𝑁 C 𝑁 ) · ( 𝑋 ↑ 𝑁 ) ) ) ) |
| 67 |
|
bcnn |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 C 𝑁 ) = 1 ) |
| 68 |
4 67
|
syl |
⊢ ( 𝜑 → ( 𝑁 C 𝑁 ) = 1 ) |
| 69 |
68
|
oveq1d |
⊢ ( 𝜑 → ( ( 𝑁 C 𝑁 ) · ( 𝑋 ↑ 𝑁 ) ) = ( 1 · ( 𝑋 ↑ 𝑁 ) ) ) |
| 70 |
38
|
mulid2d |
⊢ ( 𝜑 → ( 1 · ( 𝑋 ↑ 𝑁 ) ) = ( 𝑋 ↑ 𝑁 ) ) |
| 71 |
69 70
|
eqtrd |
⊢ ( 𝜑 → ( ( 𝑁 C 𝑁 ) · ( 𝑋 ↑ 𝑁 ) ) = ( 𝑋 ↑ 𝑁 ) ) |
| 72 |
71
|
oveq2d |
⊢ ( 𝜑 → ( Σ 𝑚 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) + ( ( 𝑁 C 𝑁 ) · ( 𝑋 ↑ 𝑁 ) ) ) = ( Σ 𝑚 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) + ( 𝑋 ↑ 𝑁 ) ) ) |
| 73 |
60 66 72
|
3eqtrd |
⊢ ( 𝜑 → ( ( 𝑋 + 1 ) ↑ 𝑁 ) = ( Σ 𝑚 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) + ( 𝑋 ↑ 𝑁 ) ) ) |
| 74 |
54 38 73
|
mvrraddd |
⊢ ( 𝜑 → ( ( ( 𝑋 + 1 ) ↑ 𝑁 ) − ( 𝑋 ↑ 𝑁 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ) |
| 75 |
|
nnm1nn0 |
⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 ) |
| 76 |
1 75
|
syl |
⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℕ0 ) |
| 77 |
76 61
|
eleqtrdi |
⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 0 ) ) |
| 78 |
|
oveq2 |
⊢ ( 𝑚 = ( 𝑁 − 1 ) → ( 𝑁 C 𝑚 ) = ( 𝑁 C ( 𝑁 − 1 ) ) ) |
| 79 |
|
oveq2 |
⊢ ( 𝑚 = ( 𝑁 − 1 ) → ( 𝑋 ↑ 𝑚 ) = ( 𝑋 ↑ ( 𝑁 − 1 ) ) ) |
| 80 |
78 79
|
oveq12d |
⊢ ( 𝑚 = ( 𝑁 − 1 ) → ( ( 𝑁 C 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) = ( ( 𝑁 C ( 𝑁 − 1 ) ) · ( 𝑋 ↑ ( 𝑁 − 1 ) ) ) ) |
| 81 |
77 53 80
|
fsumm1 |
⊢ ( 𝜑 → Σ 𝑚 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) = ( Σ 𝑚 ∈ ( 0 ... ( ( 𝑁 − 1 ) − 1 ) ) ( ( 𝑁 C 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) + ( ( 𝑁 C ( 𝑁 − 1 ) ) · ( 𝑋 ↑ ( 𝑁 − 1 ) ) ) ) ) |
| 82 |
|
1cnd |
⊢ ( 𝜑 → 1 ∈ ℂ ) |
| 83 |
22 82 82
|
subsub4d |
⊢ ( 𝜑 → ( ( 𝑁 − 1 ) − 1 ) = ( 𝑁 − ( 1 + 1 ) ) ) |
| 84 |
|
df-2 |
⊢ 2 = ( 1 + 1 ) |
| 85 |
84
|
oveq2i |
⊢ ( 𝑁 − 2 ) = ( 𝑁 − ( 1 + 1 ) ) |
| 86 |
83 85
|
eqtr4di |
⊢ ( 𝜑 → ( ( 𝑁 − 1 ) − 1 ) = ( 𝑁 − 2 ) ) |
| 87 |
86
|
oveq2d |
⊢ ( 𝜑 → ( 0 ... ( ( 𝑁 − 1 ) − 1 ) ) = ( 0 ... ( 𝑁 − 2 ) ) ) |
| 88 |
87
|
sumeq1d |
⊢ ( 𝜑 → Σ 𝑚 ∈ ( 0 ... ( ( 𝑁 − 1 ) − 1 ) ) ( ( 𝑁 C 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑁 − 2 ) ) ( ( 𝑁 C 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ) |
| 89 |
|
bcnm1 |
⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 C ( 𝑁 − 1 ) ) = 𝑁 ) |
| 90 |
4 89
|
syl |
⊢ ( 𝜑 → ( 𝑁 C ( 𝑁 − 1 ) ) = 𝑁 ) |
| 91 |
90
|
oveq1d |
⊢ ( 𝜑 → ( ( 𝑁 C ( 𝑁 − 1 ) ) · ( 𝑋 ↑ ( 𝑁 − 1 ) ) ) = ( 𝑁 · ( 𝑋 ↑ ( 𝑁 − 1 ) ) ) ) |
| 92 |
88 91
|
oveq12d |
⊢ ( 𝜑 → ( Σ 𝑚 ∈ ( 0 ... ( ( 𝑁 − 1 ) − 1 ) ) ( ( 𝑁 C 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) + ( ( 𝑁 C ( 𝑁 − 1 ) ) · ( 𝑋 ↑ ( 𝑁 − 1 ) ) ) ) = ( Σ 𝑚 ∈ ( 0 ... ( 𝑁 − 2 ) ) ( ( 𝑁 C 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) + ( 𝑁 · ( 𝑋 ↑ ( 𝑁 − 1 ) ) ) ) ) |
| 93 |
74 81 92
|
3eqtrd |
⊢ ( 𝜑 → ( ( ( 𝑋 + 1 ) ↑ 𝑁 ) − ( 𝑋 ↑ 𝑁 ) ) = ( Σ 𝑚 ∈ ( 0 ... ( 𝑁 − 2 ) ) ( ( 𝑁 C 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) + ( 𝑁 · ( 𝑋 ↑ ( 𝑁 − 1 ) ) ) ) ) |
| 94 |
|
oveq2 |
⊢ ( 𝑘 = 0 → ( 𝑁 C 𝑘 ) = ( 𝑁 C 0 ) ) |
| 95 |
|
oveq1 |
⊢ ( 𝑘 = 0 → ( 𝑘 BernPoly ( 𝑋 + 1 ) ) = ( 0 BernPoly ( 𝑋 + 1 ) ) ) |
| 96 |
|
oveq2 |
⊢ ( 𝑘 = 0 → ( 𝑁 − 𝑘 ) = ( 𝑁 − 0 ) ) |
| 97 |
96
|
oveq1d |
⊢ ( 𝑘 = 0 → ( ( 𝑁 − 𝑘 ) + 1 ) = ( ( 𝑁 − 0 ) + 1 ) ) |
| 98 |
95 97
|
oveq12d |
⊢ ( 𝑘 = 0 → ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) = ( ( 0 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 0 ) + 1 ) ) ) |
| 99 |
94 98
|
oveq12d |
⊢ ( 𝑘 = 0 → ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) = ( ( 𝑁 C 0 ) · ( ( 0 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 0 ) + 1 ) ) ) ) |
| 100 |
77 36 99
|
fsum1p |
⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) = ( ( ( 𝑁 C 0 ) · ( ( 0 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 0 ) + 1 ) ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) ) |
| 101 |
|
bpoly0 |
⊢ ( ( 𝑋 + 1 ) ∈ ℂ → ( 0 BernPoly ( 𝑋 + 1 ) ) = 1 ) |
| 102 |
6 101
|
syl |
⊢ ( 𝜑 → ( 0 BernPoly ( 𝑋 + 1 ) ) = 1 ) |
| 103 |
102
|
oveq1d |
⊢ ( 𝜑 → ( ( 0 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 0 ) + 1 ) ) = ( 1 / ( ( 𝑁 − 0 ) + 1 ) ) ) |
| 104 |
103
|
oveq2d |
⊢ ( 𝜑 → ( ( 𝑁 C 0 ) · ( ( 0 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 0 ) + 1 ) ) ) = ( ( 𝑁 C 0 ) · ( 1 / ( ( 𝑁 − 0 ) + 1 ) ) ) ) |
| 105 |
104
|
oveq1d |
⊢ ( 𝜑 → ( ( ( 𝑁 C 0 ) · ( ( 0 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 0 ) + 1 ) ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) = ( ( ( 𝑁 C 0 ) · ( 1 / ( ( 𝑁 − 0 ) + 1 ) ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) ) |
| 106 |
100 105
|
eqtrd |
⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) = ( ( ( 𝑁 C 0 ) · ( 1 / ( ( 𝑁 − 0 ) + 1 ) ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) ) |
| 107 |
|
oveq1 |
⊢ ( 𝑘 = 0 → ( 𝑘 BernPoly 𝑋 ) = ( 0 BernPoly 𝑋 ) ) |
| 108 |
107 97
|
oveq12d |
⊢ ( 𝑘 = 0 → ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) = ( ( 0 BernPoly 𝑋 ) / ( ( 𝑁 − 0 ) + 1 ) ) ) |
| 109 |
94 108
|
oveq12d |
⊢ ( 𝑘 = 0 → ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) = ( ( 𝑁 C 0 ) · ( ( 0 BernPoly 𝑋 ) / ( ( 𝑁 − 0 ) + 1 ) ) ) ) |
| 110 |
77 42 109
|
fsum1p |
⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) = ( ( ( 𝑁 C 0 ) · ( ( 0 BernPoly 𝑋 ) / ( ( 𝑁 − 0 ) + 1 ) ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) ) |
| 111 |
|
bpoly0 |
⊢ ( 𝑋 ∈ ℂ → ( 0 BernPoly 𝑋 ) = 1 ) |
| 112 |
2 111
|
syl |
⊢ ( 𝜑 → ( 0 BernPoly 𝑋 ) = 1 ) |
| 113 |
112
|
oveq1d |
⊢ ( 𝜑 → ( ( 0 BernPoly 𝑋 ) / ( ( 𝑁 − 0 ) + 1 ) ) = ( 1 / ( ( 𝑁 − 0 ) + 1 ) ) ) |
| 114 |
113
|
oveq2d |
⊢ ( 𝜑 → ( ( 𝑁 C 0 ) · ( ( 0 BernPoly 𝑋 ) / ( ( 𝑁 − 0 ) + 1 ) ) ) = ( ( 𝑁 C 0 ) · ( 1 / ( ( 𝑁 − 0 ) + 1 ) ) ) ) |
| 115 |
114
|
oveq1d |
⊢ ( 𝜑 → ( ( ( 𝑁 C 0 ) · ( ( 0 BernPoly 𝑋 ) / ( ( 𝑁 − 0 ) + 1 ) ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) = ( ( ( 𝑁 C 0 ) · ( 1 / ( ( 𝑁 − 0 ) + 1 ) ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) ) |
| 116 |
110 115
|
eqtrd |
⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) = ( ( ( 𝑁 C 0 ) · ( 1 / ( ( 𝑁 − 0 ) + 1 ) ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) ) |
| 117 |
106 116
|
oveq12d |
⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) = ( ( ( ( 𝑁 C 0 ) · ( 1 / ( ( 𝑁 − 0 ) + 1 ) ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) − ( ( ( 𝑁 C 0 ) · ( 1 / ( ( 𝑁 − 0 ) + 1 ) ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) ) ) |
| 118 |
|
0z |
⊢ 0 ∈ ℤ |
| 119 |
|
bccl |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 0 ∈ ℤ ) → ( 𝑁 C 0 ) ∈ ℕ0 ) |
| 120 |
4 118 119
|
sylancl |
⊢ ( 𝜑 → ( 𝑁 C 0 ) ∈ ℕ0 ) |
| 121 |
120
|
nn0cnd |
⊢ ( 𝜑 → ( 𝑁 C 0 ) ∈ ℂ ) |
| 122 |
22
|
subid1d |
⊢ ( 𝜑 → ( 𝑁 − 0 ) = 𝑁 ) |
| 123 |
122 1
|
eqeltrd |
⊢ ( 𝜑 → ( 𝑁 − 0 ) ∈ ℕ ) |
| 124 |
123
|
peano2nnd |
⊢ ( 𝜑 → ( ( 𝑁 − 0 ) + 1 ) ∈ ℕ ) |
| 125 |
124
|
nnrecred |
⊢ ( 𝜑 → ( 1 / ( ( 𝑁 − 0 ) + 1 ) ) ∈ ℝ ) |
| 126 |
125
|
recnd |
⊢ ( 𝜑 → ( 1 / ( ( 𝑁 − 0 ) + 1 ) ) ∈ ℂ ) |
| 127 |
121 126
|
mulcld |
⊢ ( 𝜑 → ( ( 𝑁 C 0 ) · ( 1 / ( ( 𝑁 − 0 ) + 1 ) ) ) ∈ ℂ ) |
| 128 |
|
fzfid |
⊢ ( 𝜑 → ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ∈ Fin ) |
| 129 |
|
fzp1ss |
⊢ ( 0 ∈ ℤ → ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ⊆ ( 0 ... ( 𝑁 − 1 ) ) ) |
| 130 |
118 129
|
ax-mp |
⊢ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ⊆ ( 0 ... ( 𝑁 − 1 ) ) |
| 131 |
130
|
sseli |
⊢ ( 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) |
| 132 |
131 36
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ∈ ℂ ) |
| 133 |
128 132
|
fsumcl |
⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ∈ ℂ ) |
| 134 |
131 42
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ∈ ℂ ) |
| 135 |
128 134
|
fsumcl |
⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ∈ ℂ ) |
| 136 |
127 133 135
|
pnpcand |
⊢ ( 𝜑 → ( ( ( ( 𝑁 C 0 ) · ( 1 / ( ( 𝑁 − 0 ) + 1 ) ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) − ( ( ( 𝑁 C 0 ) · ( 1 / ( ( 𝑁 − 0 ) + 1 ) ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) ) = ( Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) − Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) ) |
| 137 |
|
1zzd |
⊢ ( 𝜑 → 1 ∈ ℤ ) |
| 138 |
|
0zd |
⊢ ( 𝜑 → 0 ∈ ℤ ) |
| 139 |
1
|
nnzd |
⊢ ( 𝜑 → 𝑁 ∈ ℤ ) |
| 140 |
|
2z |
⊢ 2 ∈ ℤ |
| 141 |
|
zsubcl |
⊢ ( ( 𝑁 ∈ ℤ ∧ 2 ∈ ℤ ) → ( 𝑁 − 2 ) ∈ ℤ ) |
| 142 |
139 140 141
|
sylancl |
⊢ ( 𝜑 → ( 𝑁 − 2 ) ∈ ℤ ) |
| 143 |
|
fzssp1 |
⊢ ( 0 ... ( 𝑁 − 2 ) ) ⊆ ( 0 ... ( ( 𝑁 − 2 ) + 1 ) ) |
| 144 |
|
2cnd |
⊢ ( 𝜑 → 2 ∈ ℂ ) |
| 145 |
22 144 82
|
subsubd |
⊢ ( 𝜑 → ( 𝑁 − ( 2 − 1 ) ) = ( ( 𝑁 − 2 ) + 1 ) ) |
| 146 |
|
2m1e1 |
⊢ ( 2 − 1 ) = 1 |
| 147 |
146
|
oveq2i |
⊢ ( 𝑁 − ( 2 − 1 ) ) = ( 𝑁 − 1 ) |
| 148 |
145 147
|
eqtr3di |
⊢ ( 𝜑 → ( ( 𝑁 − 2 ) + 1 ) = ( 𝑁 − 1 ) ) |
| 149 |
148
|
oveq2d |
⊢ ( 𝜑 → ( 0 ... ( ( 𝑁 − 2 ) + 1 ) ) = ( 0 ... ( 𝑁 − 1 ) ) ) |
| 150 |
143 149
|
sseqtrid |
⊢ ( 𝜑 → ( 0 ... ( 𝑁 − 2 ) ) ⊆ ( 0 ... ( 𝑁 − 1 ) ) ) |
| 151 |
150
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑁 − 2 ) ) ) → 𝑚 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) |
| 152 |
151 53
|
syldan |
⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑁 − 2 ) ) ) → ( ( 𝑁 C 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ∈ ℂ ) |
| 153 |
|
oveq2 |
⊢ ( 𝑚 = ( 𝑘 − 1 ) → ( 𝑁 C 𝑚 ) = ( 𝑁 C ( 𝑘 − 1 ) ) ) |
| 154 |
|
oveq2 |
⊢ ( 𝑚 = ( 𝑘 − 1 ) → ( 𝑋 ↑ 𝑚 ) = ( 𝑋 ↑ ( 𝑘 − 1 ) ) ) |
| 155 |
153 154
|
oveq12d |
⊢ ( 𝑚 = ( 𝑘 − 1 ) → ( ( 𝑁 C 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) = ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( 𝑋 ↑ ( 𝑘 − 1 ) ) ) ) |
| 156 |
137 138 142 152 155
|
fsumshft |
⊢ ( 𝜑 → Σ 𝑚 ∈ ( 0 ... ( 𝑁 − 2 ) ) ( ( 𝑁 C 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) = Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( ( 𝑁 − 2 ) + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( 𝑋 ↑ ( 𝑘 − 1 ) ) ) ) |
| 157 |
148
|
oveq2d |
⊢ ( 𝜑 → ( ( 0 + 1 ) ... ( ( 𝑁 − 2 ) + 1 ) ) = ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ) |
| 158 |
157
|
sumeq1d |
⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( ( 𝑁 − 2 ) + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( 𝑋 ↑ ( 𝑘 − 1 ) ) ) = Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( 𝑋 ↑ ( 𝑘 − 1 ) ) ) ) |
| 159 |
156 158
|
eqtrd |
⊢ ( 𝜑 → Σ 𝑚 ∈ ( 0 ... ( 𝑁 − 2 ) ) ( ( 𝑁 C 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) = Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( 𝑋 ↑ ( 𝑘 − 1 ) ) ) ) |
| 160 |
|
0p1e1 |
⊢ ( 0 + 1 ) = 1 |
| 161 |
160
|
oveq1i |
⊢ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) = ( 1 ... ( 𝑁 − 1 ) ) |
| 162 |
161
|
eleq2i |
⊢ ( 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ↔ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) |
| 163 |
|
fzssp1 |
⊢ ( 1 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... ( ( 𝑁 − 1 ) + 1 ) ) |
| 164 |
25
|
oveq2d |
⊢ ( 𝜑 → ( 1 ... ( ( 𝑁 − 1 ) + 1 ) ) = ( 1 ... 𝑁 ) ) |
| 165 |
163 164
|
sseqtrid |
⊢ ( 𝜑 → ( 1 ... ( 𝑁 − 1 ) ) ⊆ ( 1 ... 𝑁 ) ) |
| 166 |
165
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ( 1 ... 𝑁 ) ) |
| 167 |
|
bcm1k |
⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( 𝑁 C 𝑘 ) = ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝑁 − ( 𝑘 − 1 ) ) / 𝑘 ) ) ) |
| 168 |
166 167
|
syl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑁 C 𝑘 ) = ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝑁 − ( 𝑘 − 1 ) ) / 𝑘 ) ) ) |
| 169 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℕ ) |
| 170 |
169
|
nncnd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℂ ) |
| 171 |
|
elfznn |
⊢ ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ℕ ) |
| 172 |
171
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ℕ ) |
| 173 |
172
|
nncnd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ℂ ) |
| 174 |
|
1cnd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 1 ∈ ℂ ) |
| 175 |
170 173 174
|
subsubd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑁 − ( 𝑘 − 1 ) ) = ( ( 𝑁 − 𝑘 ) + 1 ) ) |
| 176 |
175
|
oveq1d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 − ( 𝑘 − 1 ) ) / 𝑘 ) = ( ( ( 𝑁 − 𝑘 ) + 1 ) / 𝑘 ) ) |
| 177 |
176
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( 𝑁 − ( 𝑘 − 1 ) ) / 𝑘 ) ) = ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( 𝑁 − 𝑘 ) + 1 ) / 𝑘 ) ) ) |
| 178 |
168 177
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑁 C 𝑘 ) = ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( 𝑁 − 𝑘 ) + 1 ) / 𝑘 ) ) ) |
| 179 |
3
|
oveq1d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) − ( 𝑘 BernPoly 𝑋 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) = ( ( 𝑘 · ( 𝑋 ↑ ( 𝑘 − 1 ) ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) |
| 180 |
162 131
|
sylbir |
⊢ ( 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) |
| 181 |
180 20
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑘 BernPoly ( 𝑋 + 1 ) ) ∈ ℂ ) |
| 182 |
180 40
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑘 BernPoly 𝑋 ) ∈ ℂ ) |
| 183 |
180 33
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 − 𝑘 ) + 1 ) ∈ ℂ ) |
| 184 |
180 34
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 − 𝑘 ) + 1 ) ≠ 0 ) |
| 185 |
181 182 183 184
|
divsubdird |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) − ( 𝑘 BernPoly 𝑋 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) = ( ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) − ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) |
| 186 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑋 ∈ ℂ ) |
| 187 |
|
nnm1nn0 |
⊢ ( 𝑘 ∈ ℕ → ( 𝑘 − 1 ) ∈ ℕ0 ) |
| 188 |
172 187
|
syl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑘 − 1 ) ∈ ℕ0 ) |
| 189 |
186 188
|
expcld |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑋 ↑ ( 𝑘 − 1 ) ) ∈ ℂ ) |
| 190 |
173 189 183 184
|
div23d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑘 · ( 𝑋 ↑ ( 𝑘 − 1 ) ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) = ( ( 𝑘 / ( ( 𝑁 − 𝑘 ) + 1 ) ) · ( 𝑋 ↑ ( 𝑘 − 1 ) ) ) ) |
| 191 |
179 185 190
|
3eqtr3d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) − ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) = ( ( 𝑘 / ( ( 𝑁 − 𝑘 ) + 1 ) ) · ( 𝑋 ↑ ( 𝑘 − 1 ) ) ) ) |
| 192 |
178 191
|
oveq12d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) − ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) = ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( 𝑁 − 𝑘 ) + 1 ) / 𝑘 ) ) · ( ( 𝑘 / ( ( 𝑁 − 𝑘 ) + 1 ) ) · ( 𝑋 ↑ ( 𝑘 − 1 ) ) ) ) ) |
| 193 |
180 17
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑁 C 𝑘 ) ∈ ℂ ) |
| 194 |
181 183 184
|
divcld |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ∈ ℂ ) |
| 195 |
182 183 184
|
divcld |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ∈ ℂ ) |
| 196 |
193 194 195
|
subdid |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 C 𝑘 ) · ( ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) − ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) = ( ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) − ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) ) |
| 197 |
169
|
nnnn0d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℕ0 ) |
| 198 |
188
|
nn0zd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑘 − 1 ) ∈ ℤ ) |
| 199 |
|
bccl |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑘 − 1 ) ∈ ℤ ) → ( 𝑁 C ( 𝑘 − 1 ) ) ∈ ℕ0 ) |
| 200 |
197 198 199
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑁 C ( 𝑘 − 1 ) ) ∈ ℕ0 ) |
| 201 |
200
|
nn0cnd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑁 C ( 𝑘 − 1 ) ) ∈ ℂ ) |
| 202 |
172
|
nnne0d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → 𝑘 ≠ 0 ) |
| 203 |
183 173 202
|
divcld |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( ( 𝑁 − 𝑘 ) + 1 ) / 𝑘 ) ∈ ℂ ) |
| 204 |
173 183 184
|
divcld |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 𝑘 / ( ( 𝑁 − 𝑘 ) + 1 ) ) ∈ ℂ ) |
| 205 |
204 189
|
mulcld |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑘 / ( ( 𝑁 − 𝑘 ) + 1 ) ) · ( 𝑋 ↑ ( 𝑘 − 1 ) ) ) ∈ ℂ ) |
| 206 |
201 203 205
|
mulassd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( 𝑁 − 𝑘 ) + 1 ) / 𝑘 ) ) · ( ( 𝑘 / ( ( 𝑁 − 𝑘 ) + 1 ) ) · ( 𝑋 ↑ ( 𝑘 − 1 ) ) ) ) = ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 − 𝑘 ) + 1 ) / 𝑘 ) · ( ( 𝑘 / ( ( 𝑁 − 𝑘 ) + 1 ) ) · ( 𝑋 ↑ ( 𝑘 − 1 ) ) ) ) ) ) |
| 207 |
183 173 184 202
|
divcan6d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( ( ( 𝑁 − 𝑘 ) + 1 ) / 𝑘 ) · ( 𝑘 / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) = 1 ) |
| 208 |
207
|
oveq1d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( ( ( ( 𝑁 − 𝑘 ) + 1 ) / 𝑘 ) · ( 𝑘 / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) · ( 𝑋 ↑ ( 𝑘 − 1 ) ) ) = ( 1 · ( 𝑋 ↑ ( 𝑘 − 1 ) ) ) ) |
| 209 |
203 204 189
|
mulassd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( ( ( ( 𝑁 − 𝑘 ) + 1 ) / 𝑘 ) · ( 𝑘 / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) · ( 𝑋 ↑ ( 𝑘 − 1 ) ) ) = ( ( ( ( 𝑁 − 𝑘 ) + 1 ) / 𝑘 ) · ( ( 𝑘 / ( ( 𝑁 − 𝑘 ) + 1 ) ) · ( 𝑋 ↑ ( 𝑘 − 1 ) ) ) ) ) |
| 210 |
189
|
mulid2d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( 1 · ( 𝑋 ↑ ( 𝑘 − 1 ) ) ) = ( 𝑋 ↑ ( 𝑘 − 1 ) ) ) |
| 211 |
208 209 210
|
3eqtr3d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( ( ( 𝑁 − 𝑘 ) + 1 ) / 𝑘 ) · ( ( 𝑘 / ( ( 𝑁 − 𝑘 ) + 1 ) ) · ( 𝑋 ↑ ( 𝑘 − 1 ) ) ) ) = ( 𝑋 ↑ ( 𝑘 − 1 ) ) ) |
| 212 |
211
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( ( 𝑁 − 𝑘 ) + 1 ) / 𝑘 ) · ( ( 𝑘 / ( ( 𝑁 − 𝑘 ) + 1 ) ) · ( 𝑋 ↑ ( 𝑘 − 1 ) ) ) ) ) = ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( 𝑋 ↑ ( 𝑘 − 1 ) ) ) ) |
| 213 |
206 212
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( ( 𝑁 − 𝑘 ) + 1 ) / 𝑘 ) ) · ( ( 𝑘 / ( ( 𝑁 − 𝑘 ) + 1 ) ) · ( 𝑋 ↑ ( 𝑘 − 1 ) ) ) ) = ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( 𝑋 ↑ ( 𝑘 − 1 ) ) ) ) |
| 214 |
192 196 213
|
3eqtr3d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( 𝑁 − 1 ) ) ) → ( ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) − ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) = ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( 𝑋 ↑ ( 𝑘 − 1 ) ) ) ) |
| 215 |
162 214
|
sylan2b |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ) → ( ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) − ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) = ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( 𝑋 ↑ ( 𝑘 − 1 ) ) ) ) |
| 216 |
215
|
sumeq2dv |
⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) − ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) = Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( 𝑋 ↑ ( 𝑘 − 1 ) ) ) ) |
| 217 |
128 132 134
|
fsumsub |
⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) − ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) = ( Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) − Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) ) |
| 218 |
159 216 217
|
3eqtr2rd |
⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) − Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑁 − 2 ) ) ( ( 𝑁 C 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ) |
| 219 |
117 136 218
|
3eqtrd |
⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑁 − 2 ) ) ( ( 𝑁 C 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ) |
| 220 |
93 219
|
oveq12d |
⊢ ( 𝜑 → ( ( ( ( 𝑋 + 1 ) ↑ 𝑁 ) − ( 𝑋 ↑ 𝑁 ) ) − ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) ) = ( ( Σ 𝑚 ∈ ( 0 ... ( 𝑁 − 2 ) ) ( ( 𝑁 C 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) + ( 𝑁 · ( 𝑋 ↑ ( 𝑁 − 1 ) ) ) ) − Σ 𝑚 ∈ ( 0 ... ( 𝑁 − 2 ) ) ( ( 𝑁 C 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ) ) |
| 221 |
|
fzfid |
⊢ ( 𝜑 → ( 0 ... ( 𝑁 − 2 ) ) ∈ Fin ) |
| 222 |
221 152
|
fsumcl |
⊢ ( 𝜑 → Σ 𝑚 ∈ ( 0 ... ( 𝑁 − 2 ) ) ( ( 𝑁 C 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ∈ ℂ ) |
| 223 |
2 76
|
expcld |
⊢ ( 𝜑 → ( 𝑋 ↑ ( 𝑁 − 1 ) ) ∈ ℂ ) |
| 224 |
22 223
|
mulcld |
⊢ ( 𝜑 → ( 𝑁 · ( 𝑋 ↑ ( 𝑁 − 1 ) ) ) ∈ ℂ ) |
| 225 |
222 224
|
pncan2d |
⊢ ( 𝜑 → ( ( Σ 𝑚 ∈ ( 0 ... ( 𝑁 − 2 ) ) ( ( 𝑁 C 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) + ( 𝑁 · ( 𝑋 ↑ ( 𝑁 − 1 ) ) ) ) − Σ 𝑚 ∈ ( 0 ... ( 𝑁 − 2 ) ) ( ( 𝑁 C 𝑚 ) · ( 𝑋 ↑ 𝑚 ) ) ) = ( 𝑁 · ( 𝑋 ↑ ( 𝑁 − 1 ) ) ) ) |
| 226 |
220 225
|
eqtrd |
⊢ ( 𝜑 → ( ( ( ( 𝑋 + 1 ) ↑ 𝑁 ) − ( 𝑋 ↑ 𝑁 ) ) − ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly ( 𝑋 + 1 ) ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( 𝑘 BernPoly 𝑋 ) / ( ( 𝑁 − 𝑘 ) + 1 ) ) ) ) ) = ( 𝑁 · ( 𝑋 ↑ ( 𝑁 − 1 ) ) ) ) |
| 227 |
11 44 226
|
3eqtrd |
⊢ ( 𝜑 → ( ( 𝑁 BernPoly ( 𝑋 + 1 ) ) − ( 𝑁 BernPoly 𝑋 ) ) = ( 𝑁 · ( 𝑋 ↑ ( 𝑁 − 1 ) ) ) ) |