Step | Hyp | Ref
| Expression |
1 | | fwddifnp1.1 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
2 | | elfzelz 12717 |
. . . . . . 7
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → 𝑘 ∈ ℤ) |
3 | | bcpasc 13489 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ ℤ)
→ ((𝑁C𝑘) + (𝑁C(𝑘 − 1))) = ((𝑁 + 1)C𝑘)) |
4 | 1, 2, 3 | syl2an 586 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁C𝑘) + (𝑁C(𝑘 − 1))) = ((𝑁 + 1)C𝑘)) |
5 | 4 | oveq1d 6985 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (((𝑁C𝑘) + (𝑁C(𝑘 − 1))) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) = (((𝑁 + 1)C𝑘) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘))))) |
6 | | bccl 13490 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ ℤ)
→ (𝑁C𝑘) ∈
ℕ0) |
7 | 1, 2, 6 | syl2an 586 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑁C𝑘) ∈
ℕ0) |
8 | 7 | nn0cnd 11762 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑁C𝑘) ∈ ℂ) |
9 | | peano2zm 11831 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℤ → (𝑘 − 1) ∈
ℤ) |
10 | 2, 9 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → (𝑘 − 1) ∈ ℤ) |
11 | | bccl 13490 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝑘 − 1) ∈
ℤ) → (𝑁C(𝑘 − 1)) ∈
ℕ0) |
12 | 1, 10, 11 | syl2an 586 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑁C(𝑘 − 1)) ∈
ℕ0) |
13 | 12 | nn0cnd 11762 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑁C(𝑘 − 1)) ∈ ℂ) |
14 | 8, 13 | addcomd 10634 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁C𝑘) + (𝑁C(𝑘 − 1))) = ((𝑁C(𝑘 − 1)) + (𝑁C𝑘))) |
15 | 14 | oveq1d 6985 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (((𝑁C𝑘) + (𝑁C(𝑘 − 1))) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) = (((𝑁C(𝑘 − 1)) + (𝑁C𝑘)) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘))))) |
16 | | peano2nn0 11742 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
17 | 1, 16 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 + 1) ∈
ℕ0) |
18 | 17 | nn0zd 11891 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 + 1) ∈ ℤ) |
19 | | zsubcl 11830 |
. . . . . . . . . . . 12
⊢ (((𝑁 + 1) ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑁 + 1) − 𝑘) ∈ ℤ) |
20 | 18, 2, 19 | syl2an 586 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁 + 1) − 𝑘) ∈ ℤ) |
21 | | m1expcl 13260 |
. . . . . . . . . . 11
⊢ (((𝑁 + 1) − 𝑘) ∈ ℤ → (-1↑((𝑁 + 1) − 𝑘)) ∈ ℤ) |
22 | 20, 21 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (-1↑((𝑁 + 1) − 𝑘)) ∈ ℤ) |
23 | 22 | zcnd 11894 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (-1↑((𝑁 + 1) − 𝑘)) ∈ ℂ) |
24 | | fwddifnp1.3 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
25 | 24 | adantr 473 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝐹:𝐴⟶ℂ) |
26 | | fwddifnp1.5 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑋 + 𝑘) ∈ 𝐴) |
27 | 25, 26 | ffvelrnd 6671 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝐹‘(𝑋 + 𝑘)) ∈ ℂ) |
28 | 23, 27 | mulcld 10452 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘))) ∈ ℂ) |
29 | 13, 8, 28 | adddird 10457 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (((𝑁C(𝑘 − 1)) + (𝑁C𝑘)) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) = (((𝑁C(𝑘 − 1)) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) + ((𝑁C𝑘) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))))) |
30 | 15, 29 | eqtrd 2808 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (((𝑁C𝑘) + (𝑁C(𝑘 − 1))) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) = (((𝑁C(𝑘 − 1)) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) + ((𝑁C𝑘) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))))) |
31 | 1 | adantr 473 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝑁 ∈
ℕ0) |
32 | 31 | nn0cnd 11762 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝑁 ∈ ℂ) |
33 | 2 | adantl 474 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝑘 ∈ ℤ) |
34 | 33 | zcnd 11894 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝑘 ∈ ℂ) |
35 | | 1cnd 10426 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 1 ∈
ℂ) |
36 | 32, 34, 35 | subsub3d 10820 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑁 − (𝑘 − 1)) = ((𝑁 + 1) − 𝑘)) |
37 | 36 | eqcomd 2778 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁 + 1) − 𝑘) = (𝑁 − (𝑘 − 1))) |
38 | 37 | oveq2d 6986 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (-1↑((𝑁 + 1) − 𝑘)) = (-1↑(𝑁 − (𝑘 − 1)))) |
39 | 38 | oveq1d 6985 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘))) = ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) |
40 | 39 | oveq2d 6986 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁C(𝑘 − 1)) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) = ((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘))))) |
41 | 32, 35, 34 | addsubd 10811 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁 + 1) − 𝑘) = ((𝑁 − 𝑘) + 1)) |
42 | 41 | oveq2d 6986 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (-1↑((𝑁 + 1) − 𝑘)) = (-1↑((𝑁 − 𝑘) + 1))) |
43 | | neg1cn 11554 |
. . . . . . . . . . . . . . 15
⊢ -1 ∈
ℂ |
44 | 43 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → -1 ∈
ℂ) |
45 | | neg1ne0 11556 |
. . . . . . . . . . . . . . 15
⊢ -1 ≠
0 |
46 | 45 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → -1 ≠ 0) |
47 | 1 | nn0zd 11891 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈ ℤ) |
48 | | zsubcl 11830 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑁 − 𝑘) ∈ ℤ) |
49 | 47, 2, 48 | syl2an 586 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑁 − 𝑘) ∈ ℤ) |
50 | 44, 46, 49 | expp1zd 13327 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (-1↑((𝑁 − 𝑘) + 1)) = ((-1↑(𝑁 − 𝑘)) · -1)) |
51 | 42, 50 | eqtrd 2808 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (-1↑((𝑁 + 1) − 𝑘)) = ((-1↑(𝑁 − 𝑘)) · -1)) |
52 | | m1expcl 13260 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 − 𝑘) ∈ ℤ → (-1↑(𝑁 − 𝑘)) ∈ ℤ) |
53 | 49, 52 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (-1↑(𝑁 − 𝑘)) ∈ ℤ) |
54 | 53 | zcnd 11894 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (-1↑(𝑁 − 𝑘)) ∈ ℂ) |
55 | 54, 44 | mulcomd 10453 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((-1↑(𝑁 − 𝑘)) · -1) = (-1 ·
(-1↑(𝑁 − 𝑘)))) |
56 | 54 | mulm1d 10885 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (-1 · (-1↑(𝑁 − 𝑘))) = -(-1↑(𝑁 − 𝑘))) |
57 | 51, 55, 56 | 3eqtrd 2812 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (-1↑((𝑁 + 1) − 𝑘)) = -(-1↑(𝑁 − 𝑘))) |
58 | 57 | oveq1d 6985 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘))) = (-(-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) |
59 | 54, 27 | mulneg1d 10886 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (-(-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘))) = -((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) |
60 | 58, 59 | eqtrd 2808 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘))) = -((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) |
61 | 60 | oveq2d 6986 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁C𝑘) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) = ((𝑁C𝑘) · -((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘))))) |
62 | 54, 27 | mulcld 10452 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘))) ∈ ℂ) |
63 | 8, 62 | mulneg2d 10887 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁C𝑘) · -((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) = -((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘))))) |
64 | 61, 63 | eqtrd 2808 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁C𝑘) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) = -((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘))))) |
65 | 40, 64 | oveq12d 6988 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (((𝑁C(𝑘 − 1)) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) + ((𝑁C𝑘) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘))))) = (((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) + -((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))))) |
66 | | zsubcl 11830 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ (𝑘 − 1) ∈ ℤ)
→ (𝑁 − (𝑘 − 1)) ∈
ℤ) |
67 | 47, 10, 66 | syl2an 586 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑁 − (𝑘 − 1)) ∈ ℤ) |
68 | | m1expcl 13260 |
. . . . . . . . . . 11
⊢ ((𝑁 − (𝑘 − 1)) ∈ ℤ →
(-1↑(𝑁 − (𝑘 − 1))) ∈
ℤ) |
69 | 67, 68 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (-1↑(𝑁 − (𝑘 − 1))) ∈
ℤ) |
70 | 69 | zcnd 11894 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (-1↑(𝑁 − (𝑘 − 1))) ∈
ℂ) |
71 | 70, 27 | mulcld 10452 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘))) ∈ ℂ) |
72 | 13, 71 | mulcld 10452 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) ∈ ℂ) |
73 | 8, 62 | mulcld 10452 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) ∈ ℂ) |
74 | 72, 73 | negsubd 10796 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) + -((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘))))) = (((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) − ((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))))) |
75 | 30, 65, 74 | 3eqtrd 2812 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (((𝑁C𝑘) + (𝑁C(𝑘 − 1))) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) = (((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) − ((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))))) |
76 | 5, 75 | eqtr3d 2810 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (((𝑁 + 1)C𝑘) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) = (((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) − ((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))))) |
77 | 76 | sumeq2dv 14910 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))(((𝑁 + 1)C𝑘) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) = Σ𝑘 ∈ (0...(𝑁 + 1))(((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) − ((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))))) |
78 | | fzfid 13149 |
. . . 4
⊢ (𝜑 → (0...(𝑁 + 1)) ∈ Fin) |
79 | 78, 72, 73 | fsumsub 14993 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))(((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) − ((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘))))) = (Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) − Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))))) |
80 | | nn0uz 12087 |
. . . . . . . 8
⊢
ℕ0 = (ℤ≥‘0) |
81 | 17, 80 | syl6eleq 2870 |
. . . . . . 7
⊢ (𝜑 → (𝑁 + 1) ∈
(ℤ≥‘0)) |
82 | | oveq1 6977 |
. . . . . . . . 9
⊢ (𝑘 = 0 → (𝑘 − 1) = (0 − 1)) |
83 | 82 | oveq2d 6986 |
. . . . . . . 8
⊢ (𝑘 = 0 → (𝑁C(𝑘 − 1)) = (𝑁C(0 − 1))) |
84 | 82 | oveq2d 6986 |
. . . . . . . . . 10
⊢ (𝑘 = 0 → (𝑁 − (𝑘 − 1)) = (𝑁 − (0 − 1))) |
85 | 84 | oveq2d 6986 |
. . . . . . . . 9
⊢ (𝑘 = 0 → (-1↑(𝑁 − (𝑘 − 1))) = (-1↑(𝑁 − (0 − 1)))) |
86 | | oveq2 6978 |
. . . . . . . . . 10
⊢ (𝑘 = 0 → (𝑋 + 𝑘) = (𝑋 + 0)) |
87 | 86 | fveq2d 6497 |
. . . . . . . . 9
⊢ (𝑘 = 0 → (𝐹‘(𝑋 + 𝑘)) = (𝐹‘(𝑋 + 0))) |
88 | 85, 87 | oveq12d 6988 |
. . . . . . . 8
⊢ (𝑘 = 0 → ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘))) = ((-1↑(𝑁 − (0 − 1))) · (𝐹‘(𝑋 + 0)))) |
89 | 83, 88 | oveq12d 6988 |
. . . . . . 7
⊢ (𝑘 = 0 → ((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) = ((𝑁C(0 − 1)) · ((-1↑(𝑁 − (0 − 1)))
· (𝐹‘(𝑋 + 0))))) |
90 | 81, 72, 89 | fsum1p 14958 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) = (((𝑁C(0 − 1)) · ((-1↑(𝑁 − (0 − 1)))
· (𝐹‘(𝑋 + 0)))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))))) |
91 | | df-neg 10665 |
. . . . . . . . . . 11
⊢ -1 = (0
− 1) |
92 | 91 | oveq2i 6981 |
. . . . . . . . . 10
⊢ (𝑁C-1) = (𝑁C(0 − 1)) |
93 | | bcneg1 32428 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ (𝑁C-1) =
0) |
94 | 1, 93 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁C-1) = 0) |
95 | 92, 94 | syl5eqr 2822 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁C(0 − 1)) = 0) |
96 | 95 | oveq1d 6985 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁C(0 − 1)) · ((-1↑(𝑁 − (0 − 1)))
· (𝐹‘(𝑋 + 0)))) = (0 ·
((-1↑(𝑁 − (0
− 1))) · (𝐹‘(𝑋 + 0))))) |
97 | | 0z 11797 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℤ |
98 | | 1z 11818 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℤ |
99 | | zsubcl 11830 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℤ ∧ 1 ∈ ℤ) → (0 − 1) ∈
ℤ) |
100 | 97, 98, 99 | mp2an 679 |
. . . . . . . . . . . . . 14
⊢ (0
− 1) ∈ ℤ |
101 | 100 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0 − 1) ∈
ℤ) |
102 | 47, 101 | zsubcld 11898 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 − (0 − 1)) ∈
ℤ) |
103 | | m1expcl 13260 |
. . . . . . . . . . . 12
⊢ ((𝑁 − (0 − 1)) ∈
ℤ → (-1↑(𝑁
− (0 − 1))) ∈ ℤ) |
104 | 102, 103 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (-1↑(𝑁 − (0 − 1))) ∈
ℤ) |
105 | 104 | zcnd 11894 |
. . . . . . . . . 10
⊢ (𝜑 → (-1↑(𝑁 − (0 − 1))) ∈
ℂ) |
106 | | eluzfz1 12723 |
. . . . . . . . . . . . 13
⊢ ((𝑁 + 1) ∈
(ℤ≥‘0) → 0 ∈ (0...(𝑁 + 1))) |
107 | 81, 106 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈ (0...(𝑁 + 1))) |
108 | 26 | ralrimiva 3126 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑘 ∈ (0...(𝑁 + 1))(𝑋 + 𝑘) ∈ 𝐴) |
109 | 86 | eleq1d 2844 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 0 → ((𝑋 + 𝑘) ∈ 𝐴 ↔ (𝑋 + 0) ∈ 𝐴)) |
110 | 109 | rspcva 3527 |
. . . . . . . . . . . 12
⊢ ((0
∈ (0...(𝑁 + 1)) ∧
∀𝑘 ∈
(0...(𝑁 + 1))(𝑋 + 𝑘) ∈ 𝐴) → (𝑋 + 0) ∈ 𝐴) |
111 | 107, 108,
110 | syl2anc 576 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑋 + 0) ∈ 𝐴) |
112 | 24, 111 | ffvelrnd 6671 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘(𝑋 + 0)) ∈ ℂ) |
113 | 105, 112 | mulcld 10452 |
. . . . . . . . 9
⊢ (𝜑 → ((-1↑(𝑁 − (0 − 1)))
· (𝐹‘(𝑋 + 0))) ∈
ℂ) |
114 | 113 | mul02d 10630 |
. . . . . . . 8
⊢ (𝜑 → (0 ·
((-1↑(𝑁 − (0
− 1))) · (𝐹‘(𝑋 + 0)))) = 0) |
115 | 96, 114 | eqtrd 2808 |
. . . . . . 7
⊢ (𝜑 → ((𝑁C(0 − 1)) · ((-1↑(𝑁 − (0 − 1)))
· (𝐹‘(𝑋 + 0)))) = 0) |
116 | 115 | oveq1d 6985 |
. . . . . 6
⊢ (𝜑 → (((𝑁C(0 − 1)) · ((-1↑(𝑁 − (0 − 1)))
· (𝐹‘(𝑋 + 0)))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘))))) = (0 + Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))))) |
117 | | fzfid 13149 |
. . . . . . . 8
⊢ (𝜑 → ((0 + 1)...(𝑁 + 1)) ∈
Fin) |
118 | | olc 854 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((0 + 1)...(𝑁 + 1)) → (𝑘 = 0 ∨ 𝑘 ∈ ((0 + 1)...(𝑁 + 1)))) |
119 | | elfzp12 12795 |
. . . . . . . . . . . 12
⊢ ((𝑁 + 1) ∈
(ℤ≥‘0) → (𝑘 ∈ (0...(𝑁 + 1)) ↔ (𝑘 = 0 ∨ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))))) |
120 | 81, 119 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑘 ∈ (0...(𝑁 + 1)) ↔ (𝑘 = 0 ∨ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))))) |
121 | 120 | biimpar 470 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 = 0 ∨ 𝑘 ∈ ((0 + 1)...(𝑁 + 1)))) → 𝑘 ∈ (0...(𝑁 + 1))) |
122 | 118, 121 | sylan2 583 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑘 ∈ (0...(𝑁 + 1))) |
123 | 122, 72 | syldan 582 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) ∈ ℂ) |
124 | 117, 123 | fsumcl 14940 |
. . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) ∈ ℂ) |
125 | 124 | addid2d 10633 |
. . . . . 6
⊢ (𝜑 → (0 + Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘))))) = Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘))))) |
126 | 90, 116, 125 | 3eqtrd 2812 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) = Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘))))) |
127 | | fwddifnp1.4 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ ℂ) |
128 | 127 | adantr 473 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑋 ∈ ℂ) |
129 | | 1cnd 10426 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → 1 ∈
ℂ) |
130 | | elfzelz 12717 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ((0 + 1)...(𝑁 + 1)) → 𝑘 ∈ ℤ) |
131 | 130 | zcnd 11894 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ((0 + 1)...(𝑁 + 1)) → 𝑘 ∈ ℂ) |
132 | 131 | adantl 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑘 ∈ ℂ) |
133 | 128, 129,
132 | ppncand 10830 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑋 + 1) + (𝑘 − 1)) = (𝑋 + 𝑘)) |
134 | 133 | fveq2d 6497 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → (𝐹‘((𝑋 + 1) + (𝑘 − 1))) = (𝐹‘(𝑋 + 𝑘))) |
135 | 134 | oveq2d 6986 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘((𝑋 + 1) + (𝑘 − 1)))) = ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) |
136 | 135 | oveq2d 6986 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘((𝑋 + 1) + (𝑘 − 1))))) = ((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘))))) |
137 | 136 | sumeq2dv 14910 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘((𝑋 + 1) + (𝑘 − 1))))) = Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘))))) |
138 | | oveq2 6978 |
. . . . . . . 8
⊢ (𝑗 = 𝑘 → (𝑁C𝑗) = (𝑁C𝑘)) |
139 | | oveq2 6978 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑘 → (𝑁 − 𝑗) = (𝑁 − 𝑘)) |
140 | 139 | oveq2d 6986 |
. . . . . . . . 9
⊢ (𝑗 = 𝑘 → (-1↑(𝑁 − 𝑗)) = (-1↑(𝑁 − 𝑘))) |
141 | | oveq2 6978 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑘 → ((𝑋 + 1) + 𝑗) = ((𝑋 + 1) + 𝑘)) |
142 | 141 | fveq2d 6497 |
. . . . . . . . 9
⊢ (𝑗 = 𝑘 → (𝐹‘((𝑋 + 1) + 𝑗)) = (𝐹‘((𝑋 + 1) + 𝑘))) |
143 | 140, 142 | oveq12d 6988 |
. . . . . . . 8
⊢ (𝑗 = 𝑘 → ((-1↑(𝑁 − 𝑗)) · (𝐹‘((𝑋 + 1) + 𝑗))) = ((-1↑(𝑁 − 𝑘)) · (𝐹‘((𝑋 + 1) + 𝑘)))) |
144 | 138, 143 | oveq12d 6988 |
. . . . . . 7
⊢ (𝑗 = 𝑘 → ((𝑁C𝑗) · ((-1↑(𝑁 − 𝑗)) · (𝐹‘((𝑋 + 1) + 𝑗)))) = ((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘((𝑋 + 1) + 𝑘))))) |
145 | 144 | cbvsumv 14903 |
. . . . . 6
⊢
Σ𝑗 ∈
(0...𝑁)((𝑁C𝑗) · ((-1↑(𝑁 − 𝑗)) · (𝐹‘((𝑋 + 1) + 𝑗)))) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘((𝑋 + 1) + 𝑘)))) |
146 | | 1zzd 11819 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℤ) |
147 | | 0zd 11798 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℤ) |
148 | | elfzelz 12717 |
. . . . . . . . 9
⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ) |
149 | | bccl 13490 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑗 ∈ ℤ)
→ (𝑁C𝑗) ∈
ℕ0) |
150 | 149 | nn0cnd 11762 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑗 ∈ ℤ)
→ (𝑁C𝑗) ∈
ℂ) |
151 | 1, 148, 150 | syl2an 586 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑁C𝑗) ∈ ℂ) |
152 | | zsubcl 11830 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (𝑁 − 𝑗) ∈ ℤ) |
153 | 47, 148, 152 | syl2an 586 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑁 − 𝑗) ∈ ℤ) |
154 | | m1expcl 13260 |
. . . . . . . . . . 11
⊢ ((𝑁 − 𝑗) ∈ ℤ → (-1↑(𝑁 − 𝑗)) ∈ ℤ) |
155 | 153, 154 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (-1↑(𝑁 − 𝑗)) ∈ ℤ) |
156 | 155 | zcnd 11894 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (-1↑(𝑁 − 𝑗)) ∈ ℂ) |
157 | 24 | adantr 473 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝐹:𝐴⟶ℂ) |
158 | 127 | adantr 473 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑋 ∈ ℂ) |
159 | | 1cnd 10426 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 1 ∈ ℂ) |
160 | 148 | zcnd 11894 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℂ) |
161 | 160 | adantl 474 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ ℂ) |
162 | 158, 159,
161 | addassd 10454 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑋 + 1) + 𝑗) = (𝑋 + (1 + 𝑗))) |
163 | 159, 161 | addcomd 10634 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (1 + 𝑗) = (𝑗 + 1)) |
164 | 163 | oveq2d 6986 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑋 + (1 + 𝑗)) = (𝑋 + (𝑗 + 1))) |
165 | 162, 164 | eqtrd 2808 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑋 + 1) + 𝑗) = (𝑋 + (𝑗 + 1))) |
166 | | fzp1elp1 12769 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ (0...(𝑁 + 1))) |
167 | | oveq2 6978 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = (𝑗 + 1) → (𝑋 + 𝑘) = (𝑋 + (𝑗 + 1))) |
168 | 167 | eleq1d 2844 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = (𝑗 + 1) → ((𝑋 + 𝑘) ∈ 𝐴 ↔ (𝑋 + (𝑗 + 1)) ∈ 𝐴)) |
169 | 168 | rspccv 3526 |
. . . . . . . . . . . . . 14
⊢
(∀𝑘 ∈
(0...(𝑁 + 1))(𝑋 + 𝑘) ∈ 𝐴 → ((𝑗 + 1) ∈ (0...(𝑁 + 1)) → (𝑋 + (𝑗 + 1)) ∈ 𝐴)) |
170 | 108, 169 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑗 + 1) ∈ (0...(𝑁 + 1)) → (𝑋 + (𝑗 + 1)) ∈ 𝐴)) |
171 | 170 | imp 398 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑗 + 1) ∈ (0...(𝑁 + 1))) → (𝑋 + (𝑗 + 1)) ∈ 𝐴) |
172 | 166, 171 | sylan2 583 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑋 + (𝑗 + 1)) ∈ 𝐴) |
173 | 165, 172 | eqeltrd 2860 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑋 + 1) + 𝑗) ∈ 𝐴) |
174 | 157, 173 | ffvelrnd 6671 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐹‘((𝑋 + 1) + 𝑗)) ∈ ℂ) |
175 | 156, 174 | mulcld 10452 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((-1↑(𝑁 − 𝑗)) · (𝐹‘((𝑋 + 1) + 𝑗))) ∈ ℂ) |
176 | 151, 175 | mulcld 10452 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑁C𝑗) · ((-1↑(𝑁 − 𝑗)) · (𝐹‘((𝑋 + 1) + 𝑗)))) ∈ ℂ) |
177 | | oveq2 6978 |
. . . . . . . 8
⊢ (𝑗 = (𝑘 − 1) → (𝑁C𝑗) = (𝑁C(𝑘 − 1))) |
178 | | oveq2 6978 |
. . . . . . . . . 10
⊢ (𝑗 = (𝑘 − 1) → (𝑁 − 𝑗) = (𝑁 − (𝑘 − 1))) |
179 | 178 | oveq2d 6986 |
. . . . . . . . 9
⊢ (𝑗 = (𝑘 − 1) → (-1↑(𝑁 − 𝑗)) = (-1↑(𝑁 − (𝑘 − 1)))) |
180 | | oveq2 6978 |
. . . . . . . . . 10
⊢ (𝑗 = (𝑘 − 1) → ((𝑋 + 1) + 𝑗) = ((𝑋 + 1) + (𝑘 − 1))) |
181 | 180 | fveq2d 6497 |
. . . . . . . . 9
⊢ (𝑗 = (𝑘 − 1) → (𝐹‘((𝑋 + 1) + 𝑗)) = (𝐹‘((𝑋 + 1) + (𝑘 − 1)))) |
182 | 179, 181 | oveq12d 6988 |
. . . . . . . 8
⊢ (𝑗 = (𝑘 − 1) → ((-1↑(𝑁 − 𝑗)) · (𝐹‘((𝑋 + 1) + 𝑗))) = ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘((𝑋 + 1) + (𝑘 − 1))))) |
183 | 177, 182 | oveq12d 6988 |
. . . . . . 7
⊢ (𝑗 = (𝑘 − 1) → ((𝑁C𝑗) · ((-1↑(𝑁 − 𝑗)) · (𝐹‘((𝑋 + 1) + 𝑗)))) = ((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘((𝑋 + 1) + (𝑘 − 1)))))) |
184 | 146, 147,
47, 176, 183 | fsumshft 14985 |
. . . . . 6
⊢ (𝜑 → Σ𝑗 ∈ (0...𝑁)((𝑁C𝑗) · ((-1↑(𝑁 − 𝑗)) · (𝐹‘((𝑋 + 1) + 𝑗)))) = Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘((𝑋 + 1) + (𝑘 − 1)))))) |
185 | 145, 184 | syl5reqr 2823 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘((𝑋 + 1) + (𝑘 − 1))))) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘((𝑋 + 1) + 𝑘))))) |
186 | 126, 137,
185 | 3eqtr2d 2814 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘((𝑋 + 1) + 𝑘))))) |
187 | 1, 80 | syl6eleq 2870 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘0)) |
188 | | oveq2 6978 |
. . . . . . 7
⊢ (𝑘 = (𝑁 + 1) → (𝑁C𝑘) = (𝑁C(𝑁 + 1))) |
189 | | oveq2 6978 |
. . . . . . . . 9
⊢ (𝑘 = (𝑁 + 1) → (𝑁 − 𝑘) = (𝑁 − (𝑁 + 1))) |
190 | 189 | oveq2d 6986 |
. . . . . . . 8
⊢ (𝑘 = (𝑁 + 1) → (-1↑(𝑁 − 𝑘)) = (-1↑(𝑁 − (𝑁 + 1)))) |
191 | | oveq2 6978 |
. . . . . . . . 9
⊢ (𝑘 = (𝑁 + 1) → (𝑋 + 𝑘) = (𝑋 + (𝑁 + 1))) |
192 | 191 | fveq2d 6497 |
. . . . . . . 8
⊢ (𝑘 = (𝑁 + 1) → (𝐹‘(𝑋 + 𝑘)) = (𝐹‘(𝑋 + (𝑁 + 1)))) |
193 | 190, 192 | oveq12d 6988 |
. . . . . . 7
⊢ (𝑘 = (𝑁 + 1) → ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘))) = ((-1↑(𝑁 − (𝑁 + 1))) · (𝐹‘(𝑋 + (𝑁 + 1))))) |
194 | 188, 193 | oveq12d 6988 |
. . . . . 6
⊢ (𝑘 = (𝑁 + 1) → ((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) = ((𝑁C(𝑁 + 1)) · ((-1↑(𝑁 − (𝑁 + 1))) · (𝐹‘(𝑋 + (𝑁 + 1)))))) |
195 | 187, 73, 194 | fsump1 14961 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) = (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) + ((𝑁C(𝑁 + 1)) · ((-1↑(𝑁 − (𝑁 + 1))) · (𝐹‘(𝑋 + (𝑁 + 1))))))) |
196 | | bcval 13472 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝑁 + 1) ∈
ℤ) → (𝑁C(𝑁 + 1)) = if((𝑁 + 1) ∈ (0...𝑁), ((!‘𝑁) / ((!‘(𝑁 − (𝑁 + 1))) · (!‘(𝑁 + 1)))), 0)) |
197 | 1, 18, 196 | syl2anc 576 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁C(𝑁 + 1)) = if((𝑁 + 1) ∈ (0...𝑁), ((!‘𝑁) / ((!‘(𝑁 − (𝑁 + 1))) · (!‘(𝑁 + 1)))), 0)) |
198 | | fzp1nel 12800 |
. . . . . . . . . 10
⊢ ¬
(𝑁 + 1) ∈ (0...𝑁) |
199 | 198 | iffalsei 4354 |
. . . . . . . . 9
⊢ if((𝑁 + 1) ∈ (0...𝑁), ((!‘𝑁) / ((!‘(𝑁 − (𝑁 + 1))) · (!‘(𝑁 + 1)))), 0) = 0 |
200 | 197, 199 | syl6eq 2824 |
. . . . . . . 8
⊢ (𝜑 → (𝑁C(𝑁 + 1)) = 0) |
201 | 200 | oveq1d 6985 |
. . . . . . 7
⊢ (𝜑 → ((𝑁C(𝑁 + 1)) · ((-1↑(𝑁 − (𝑁 + 1))) · (𝐹‘(𝑋 + (𝑁 + 1))))) = (0 · ((-1↑(𝑁 − (𝑁 + 1))) · (𝐹‘(𝑋 + (𝑁 + 1)))))) |
202 | 47, 18 | zsubcld 11898 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 − (𝑁 + 1)) ∈ ℤ) |
203 | | m1expcl 13260 |
. . . . . . . . . . 11
⊢ ((𝑁 − (𝑁 + 1)) ∈ ℤ → (-1↑(𝑁 − (𝑁 + 1))) ∈ ℤ) |
204 | 203 | zcnd 11894 |
. . . . . . . . . 10
⊢ ((𝑁 − (𝑁 + 1)) ∈ ℤ → (-1↑(𝑁 − (𝑁 + 1))) ∈ ℂ) |
205 | 202, 204 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (-1↑(𝑁 − (𝑁 + 1))) ∈ ℂ) |
206 | | eluzfz2 12724 |
. . . . . . . . . . . 12
⊢ ((𝑁 + 1) ∈
(ℤ≥‘0) → (𝑁 + 1) ∈ (0...(𝑁 + 1))) |
207 | 81, 206 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 + 1) ∈ (0...(𝑁 + 1))) |
208 | 191 | eleq1d 2844 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝑁 + 1) → ((𝑋 + 𝑘) ∈ 𝐴 ↔ (𝑋 + (𝑁 + 1)) ∈ 𝐴)) |
209 | 208 | rspcv 3525 |
. . . . . . . . . . 11
⊢ ((𝑁 + 1) ∈ (0...(𝑁 + 1)) → (∀𝑘 ∈ (0...(𝑁 + 1))(𝑋 + 𝑘) ∈ 𝐴 → (𝑋 + (𝑁 + 1)) ∈ 𝐴)) |
210 | 207, 108,
209 | sylc 65 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 + (𝑁 + 1)) ∈ 𝐴) |
211 | 24, 210 | ffvelrnd 6671 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘(𝑋 + (𝑁 + 1))) ∈ ℂ) |
212 | 205, 211 | mulcld 10452 |
. . . . . . . 8
⊢ (𝜑 → ((-1↑(𝑁 − (𝑁 + 1))) · (𝐹‘(𝑋 + (𝑁 + 1)))) ∈ ℂ) |
213 | 212 | mul02d 10630 |
. . . . . . 7
⊢ (𝜑 → (0 ·
((-1↑(𝑁 − (𝑁 + 1))) · (𝐹‘(𝑋 + (𝑁 + 1))))) = 0) |
214 | 201, 213 | eqtrd 2808 |
. . . . . 6
⊢ (𝜑 → ((𝑁C(𝑁 + 1)) · ((-1↑(𝑁 − (𝑁 + 1))) · (𝐹‘(𝑋 + (𝑁 + 1))))) = 0) |
215 | 214 | oveq2d 6986 |
. . . . 5
⊢ (𝜑 → (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) + ((𝑁C(𝑁 + 1)) · ((-1↑(𝑁 − (𝑁 + 1))) · (𝐹‘(𝑋 + (𝑁 + 1)))))) = (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) + 0)) |
216 | | fzfid 13149 |
. . . . . . 7
⊢ (𝜑 → (0...𝑁) ∈ Fin) |
217 | | fzelp1 12768 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ (0...(𝑁 + 1))) |
218 | 217, 73 | sylan2 583 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) ∈ ℂ) |
219 | 216, 218 | fsumcl 14940 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) ∈ ℂ) |
220 | 219 | addid1d 10632 |
. . . . 5
⊢ (𝜑 → (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) + 0) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘))))) |
221 | 195, 215,
220 | 3eqtrd 2812 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘))))) |
222 | 186, 221 | oveq12d 6988 |
. . 3
⊢ (𝜑 → (Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) − Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘))))) = (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘((𝑋 + 1) + 𝑘)))) − Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))))) |
223 | 77, 79, 222 | 3eqtrd 2812 |
. 2
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))(((𝑁 + 1)C𝑘) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) = (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘((𝑋 + 1) + 𝑘)))) − Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))))) |
224 | | fwddifnp1.2 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
225 | 17, 224, 24, 127, 26 | fwddifnval 33085 |
. 2
⊢ (𝜑 → (((𝑁 + 1) △n 𝐹)‘𝑋) = Σ𝑘 ∈ (0...(𝑁 + 1))(((𝑁 + 1)C𝑘) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘))))) |
226 | | peano2cn 10604 |
. . . . 5
⊢ (𝑋 ∈ ℂ → (𝑋 + 1) ∈
ℂ) |
227 | 127, 226 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑋 + 1) ∈ ℂ) |
228 | 127 | adantr 473 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑋 ∈ ℂ) |
229 | | 1cnd 10426 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 1 ∈ ℂ) |
230 | | elfzelz 12717 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℤ) |
231 | 230 | zcnd 11894 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℂ) |
232 | 231 | adantl 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℂ) |
233 | 228, 229,
232 | addassd 10454 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑋 + 1) + 𝑘) = (𝑋 + (1 + 𝑘))) |
234 | 229, 232 | addcomd 10634 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (1 + 𝑘) = (𝑘 + 1)) |
235 | 234 | oveq2d 6986 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑋 + (1 + 𝑘)) = (𝑋 + (𝑘 + 1))) |
236 | 233, 235 | eqtrd 2808 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑋 + 1) + 𝑘) = (𝑋 + (𝑘 + 1))) |
237 | | fzp1elp1 12769 |
. . . . . 6
⊢ (𝑘 ∈ (0...𝑁) → (𝑘 + 1) ∈ (0...(𝑁 + 1))) |
238 | | oveq1 6977 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑘 → (𝑗 + 1) = (𝑘 + 1)) |
239 | 238 | eleq1d 2844 |
. . . . . . . . 9
⊢ (𝑗 = 𝑘 → ((𝑗 + 1) ∈ (0...(𝑁 + 1)) ↔ (𝑘 + 1) ∈ (0...(𝑁 + 1)))) |
240 | 239 | anbi2d 619 |
. . . . . . . 8
⊢ (𝑗 = 𝑘 → ((𝜑 ∧ (𝑗 + 1) ∈ (0...(𝑁 + 1))) ↔ (𝜑 ∧ (𝑘 + 1) ∈ (0...(𝑁 + 1))))) |
241 | 238 | oveq2d 6986 |
. . . . . . . . 9
⊢ (𝑗 = 𝑘 → (𝑋 + (𝑗 + 1)) = (𝑋 + (𝑘 + 1))) |
242 | 241 | eleq1d 2844 |
. . . . . . . 8
⊢ (𝑗 = 𝑘 → ((𝑋 + (𝑗 + 1)) ∈ 𝐴 ↔ (𝑋 + (𝑘 + 1)) ∈ 𝐴)) |
243 | 240, 242 | imbi12d 337 |
. . . . . . 7
⊢ (𝑗 = 𝑘 → (((𝜑 ∧ (𝑗 + 1) ∈ (0...(𝑁 + 1))) → (𝑋 + (𝑗 + 1)) ∈ 𝐴) ↔ ((𝜑 ∧ (𝑘 + 1) ∈ (0...(𝑁 + 1))) → (𝑋 + (𝑘 + 1)) ∈ 𝐴))) |
244 | 243, 171 | chvarv 2325 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (0...(𝑁 + 1))) → (𝑋 + (𝑘 + 1)) ∈ 𝐴) |
245 | 237, 244 | sylan2 583 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑋 + (𝑘 + 1)) ∈ 𝐴) |
246 | 236, 245 | eqeltrd 2860 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑋 + 1) + 𝑘) ∈ 𝐴) |
247 | 1, 224, 24, 227, 246 | fwddifnval 33085 |
. . 3
⊢ (𝜑 → ((𝑁 △n 𝐹)‘(𝑋 + 1)) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘((𝑋 + 1) + 𝑘))))) |
248 | 217, 26 | sylan2 583 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑋 + 𝑘) ∈ 𝐴) |
249 | 1, 224, 24, 127, 248 | fwddifnval 33085 |
. . 3
⊢ (𝜑 → ((𝑁 △n 𝐹)‘𝑋) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘))))) |
250 | 247, 249 | oveq12d 6988 |
. 2
⊢ (𝜑 → (((𝑁 △n 𝐹)‘(𝑋 + 1)) − ((𝑁 △n 𝐹)‘𝑋)) = (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘((𝑋 + 1) + 𝑘)))) − Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))))) |
251 | 223, 225,
250 | 3eqtr4d 2818 |
1
⊢ (𝜑 → (((𝑁 + 1) △n 𝐹)‘𝑋) = (((𝑁 △n 𝐹)‘(𝑋 + 1)) − ((𝑁 △n 𝐹)‘𝑋))) |