Step | Hyp | Ref
| Expression |
1 | | elfzelz 13254 |
. . . . . . 7
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℤ) |
2 | | bcpascm1 45654 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ) → (((𝑁 − 1)C𝑘) + ((𝑁 − 1)C(𝑘 − 1))) = (𝑁C𝑘)) |
3 | 1, 2 | sylan2 593 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → (((𝑁 − 1)C𝑘) + ((𝑁 − 1)C(𝑘 − 1))) = (𝑁C𝑘)) |
4 | 3 | eqcomd 2744 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → (𝑁C𝑘) = (((𝑁 − 1)C𝑘) + ((𝑁 − 1)C(𝑘 − 1)))) |
5 | 4 | oveq2d 7293 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((-1↑𝑘) · (𝑁C𝑘)) = ((-1↑𝑘) · (((𝑁 − 1)C𝑘) + ((𝑁 − 1)C(𝑘 − 1))))) |
6 | | ax-1cn 10927 |
. . . . . . 7
⊢ 1 ∈
ℂ |
7 | | negcl 11219 |
. . . . . . . 8
⊢ (1 ∈
ℂ → -1 ∈ ℂ) |
8 | | elfznn0 13347 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) |
9 | | expcl 13798 |
. . . . . . . 8
⊢ ((-1
∈ ℂ ∧ 𝑘
∈ ℕ0) → (-1↑𝑘) ∈ ℂ) |
10 | 7, 8, 9 | syl2an 596 |
. . . . . . 7
⊢ ((1
∈ ℂ ∧ 𝑘
∈ (0...𝑁)) →
(-1↑𝑘) ∈
ℂ) |
11 | 6, 10 | mpan 687 |
. . . . . 6
⊢ (𝑘 ∈ (0...𝑁) → (-1↑𝑘) ∈ ℂ) |
12 | 11 | adantl 482 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → (-1↑𝑘) ∈ ℂ) |
13 | | nnm1nn0 12272 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
14 | | bccl 14034 |
. . . . . . 7
⊢ (((𝑁 − 1) ∈
ℕ0 ∧ 𝑘
∈ ℤ) → ((𝑁
− 1)C𝑘) ∈
ℕ0) |
15 | 14 | nn0cnd 12293 |
. . . . . 6
⊢ (((𝑁 − 1) ∈
ℕ0 ∧ 𝑘
∈ ℤ) → ((𝑁
− 1)C𝑘) ∈
ℂ) |
16 | 13, 1, 15 | syl2an 596 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁 − 1)C𝑘) ∈ ℂ) |
17 | | peano2zm 12361 |
. . . . . . 7
⊢ (𝑘 ∈ ℤ → (𝑘 − 1) ∈
ℤ) |
18 | 1, 17 | syl 17 |
. . . . . 6
⊢ (𝑘 ∈ (0...𝑁) → (𝑘 − 1) ∈ ℤ) |
19 | | bccl 14034 |
. . . . . . 7
⊢ (((𝑁 − 1) ∈
ℕ0 ∧ (𝑘 − 1) ∈ ℤ) → ((𝑁 − 1)C(𝑘 − 1)) ∈
ℕ0) |
20 | 19 | nn0cnd 12293 |
. . . . . 6
⊢ (((𝑁 − 1) ∈
ℕ0 ∧ (𝑘 − 1) ∈ ℤ) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℂ) |
21 | 13, 18, 20 | syl2an 596 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℂ) |
22 | 12, 16, 21 | adddid 10997 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((-1↑𝑘) · (((𝑁 − 1)C𝑘) + ((𝑁 − 1)C(𝑘 − 1)))) = (((-1↑𝑘) · ((𝑁 − 1)C𝑘)) + ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))))) |
23 | 5, 22 | eqtrd 2778 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((-1↑𝑘) · (𝑁C𝑘)) = (((-1↑𝑘) · ((𝑁 − 1)C𝑘)) + ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))))) |
24 | 23 | sumeq2dv 15413 |
. 2
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · (𝑁C𝑘)) = Σ𝑘 ∈ (0...𝑁)(((-1↑𝑘) · ((𝑁 − 1)C𝑘)) + ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))))) |
25 | | fzfid 13691 |
. . . 4
⊢ (𝑁 ∈ ℕ →
(0...𝑁) ∈
Fin) |
26 | | neg1cn 12085 |
. . . . . . 7
⊢ -1 ∈
ℂ |
27 | 26 | a1i 11 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → -1 ∈
ℂ) |
28 | 27, 8, 9 | syl2an 596 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → (-1↑𝑘) ∈ ℂ) |
29 | 28, 16 | mulcld 10993 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((-1↑𝑘) · ((𝑁 − 1)C𝑘)) ∈ ℂ) |
30 | | 1z 12348 |
. . . . . . . 8
⊢ 1 ∈
ℤ |
31 | 30 | a1i 11 |
. . . . . . 7
⊢ (𝑘 ∈ (0...𝑁) → 1 ∈ ℤ) |
32 | 1, 31 | zsubcld 12429 |
. . . . . 6
⊢ (𝑘 ∈ (0...𝑁) → (𝑘 − 1) ∈ ℤ) |
33 | 13, 32, 20 | syl2an 596 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℂ) |
34 | 28, 33 | mulcld 10993 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) ∈
ℂ) |
35 | 25, 29, 34 | fsumadd 15450 |
. . 3
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ (0...𝑁)(((-1↑𝑘) · ((𝑁 − 1)C𝑘)) + ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1)))) = (Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · ((𝑁 − 1)C𝑘)) + Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))))) |
36 | 30 | a1i 11 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 1 ∈
ℤ) |
37 | | 0zd 12329 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 0 ∈
ℤ) |
38 | | nnz 12340 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
39 | | oveq2 7285 |
. . . . . . 7
⊢ (𝑘 = (𝑗 − 1) → (-1↑𝑘) = (-1↑(𝑗 − 1))) |
40 | | oveq2 7285 |
. . . . . . 7
⊢ (𝑘 = (𝑗 − 1) → ((𝑁 − 1)C𝑘) = ((𝑁 − 1)C(𝑗 − 1))) |
41 | 39, 40 | oveq12d 7295 |
. . . . . 6
⊢ (𝑘 = (𝑗 − 1) → ((-1↑𝑘) · ((𝑁 − 1)C𝑘)) = ((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1)))) |
42 | 36, 37, 38, 29, 41 | fsumshft 15490 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · ((𝑁 − 1)C𝑘)) = Σ𝑗 ∈ ((0 + 1)...(𝑁 + 1))((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1)))) |
43 | | 0p1e1 12093 |
. . . . . . . 8
⊢ (0 + 1) =
1 |
44 | 43 | oveq1i 7287 |
. . . . . . 7
⊢ ((0 +
1)...(𝑁 + 1)) = (1...(𝑁 + 1)) |
45 | 44 | a1i 11 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → ((0 +
1)...(𝑁 + 1)) = (1...(𝑁 + 1))) |
46 | 45 | sumeq1d 15411 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ ((0 +
1)...(𝑁 +
1))((-1↑(𝑗 − 1))
· ((𝑁 −
1)C(𝑗 − 1))) =
Σ𝑗 ∈ (1...(𝑁 + 1))((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1)))) |
47 | | elnnuz 12620 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈
(ℤ≥‘1)) |
48 | 47 | biimpi 215 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
(ℤ≥‘1)) |
49 | 26 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → -1 ∈
ℂ) |
50 | | elfznn 13283 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (1...(𝑁 + 1)) → 𝑗 ∈ ℕ) |
51 | | nnm1nn0 12272 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → (𝑗 − 1) ∈
ℕ0) |
52 | 50, 51 | syl 17 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (1...(𝑁 + 1)) → (𝑗 − 1) ∈
ℕ0) |
53 | 52 | adantl 482 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → (𝑗 − 1) ∈
ℕ0) |
54 | 49, 53 | expcld 13862 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → (-1↑(𝑗 − 1)) ∈ ℂ) |
55 | | elfzelz 13254 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (1...(𝑁 + 1)) → 𝑗 ∈ ℤ) |
56 | | elfzel1 13253 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (1...(𝑁 + 1)) → 1 ∈
ℤ) |
57 | 55, 56 | zsubcld 12429 |
. . . . . . . . 9
⊢ (𝑗 ∈ (1...(𝑁 + 1)) → (𝑗 − 1) ∈ ℤ) |
58 | | bccl 14034 |
. . . . . . . . . 10
⊢ (((𝑁 − 1) ∈
ℕ0 ∧ (𝑗 − 1) ∈ ℤ) → ((𝑁 − 1)C(𝑗 − 1)) ∈
ℕ0) |
59 | 58 | nn0cnd 12293 |
. . . . . . . . 9
⊢ (((𝑁 − 1) ∈
ℕ0 ∧ (𝑗 − 1) ∈ ℤ) → ((𝑁 − 1)C(𝑗 − 1)) ∈ ℂ) |
60 | 13, 57, 59 | syl2an 596 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → ((𝑁 − 1)C(𝑗 − 1)) ∈ ℂ) |
61 | 54, 60 | mulcld 10993 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → ((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) ∈
ℂ) |
62 | | oveq1 7284 |
. . . . . . . . 9
⊢ (𝑗 = (𝑁 + 1) → (𝑗 − 1) = ((𝑁 + 1) − 1)) |
63 | 62 | oveq2d 7293 |
. . . . . . . 8
⊢ (𝑗 = (𝑁 + 1) → (-1↑(𝑗 − 1)) = (-1↑((𝑁 + 1) − 1))) |
64 | 62 | oveq2d 7293 |
. . . . . . . 8
⊢ (𝑗 = (𝑁 + 1) → ((𝑁 − 1)C(𝑗 − 1)) = ((𝑁 − 1)C((𝑁 + 1) − 1))) |
65 | 63, 64 | oveq12d 7295 |
. . . . . . 7
⊢ (𝑗 = (𝑁 + 1) → ((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = ((-1↑((𝑁 + 1) − 1)) · ((𝑁 − 1)C((𝑁 + 1) − 1)))) |
66 | 48, 61, 65 | fsump1 15466 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ (1...(𝑁 + 1))((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = (Σ𝑗 ∈ (1...𝑁)((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) + ((-1↑((𝑁 + 1) − 1)) · ((𝑁 − 1)C((𝑁 + 1) − 1))))) |
67 | | nncn 11979 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
68 | | pncan1 11397 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁) |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = 𝑁) |
70 | | nnnn0 12238 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
71 | 69, 70 | eqeltrd 2839 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) ∈
ℕ0) |
72 | 71 | nn0zd 12422 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) ∈
ℤ) |
73 | | nnre 11978 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
74 | | ltm1 11815 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℝ → (𝑁 − 1) < 𝑁) |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) < 𝑁) |
76 | 75, 69 | breqtrrd 5104 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) < ((𝑁 + 1) −
1)) |
77 | 76 | olcd 871 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) − 1) < 0 ∨
(𝑁 − 1) < ((𝑁 + 1) −
1))) |
78 | | bcval4 14019 |
. . . . . . . . . 10
⊢ (((𝑁 − 1) ∈
ℕ0 ∧ ((𝑁 + 1) − 1) ∈ ℤ ∧
(((𝑁 + 1) − 1) < 0
∨ (𝑁 − 1) <
((𝑁 + 1) − 1)))
→ ((𝑁 −
1)C((𝑁 + 1) − 1)) =
0) |
79 | 13, 72, 77, 78 | syl3anc 1370 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1)C((𝑁 + 1) − 1)) = 0) |
80 | 79 | oveq2d 7293 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
((-1↑((𝑁 + 1) −
1)) · ((𝑁 −
1)C((𝑁 + 1) − 1))) =
((-1↑((𝑁 + 1) −
1)) · 0)) |
81 | 27, 71 | expcld 13862 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(-1↑((𝑁 + 1) −
1)) ∈ ℂ) |
82 | 81 | mul01d 11172 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
((-1↑((𝑁 + 1) −
1)) · 0) = 0) |
83 | 80, 82 | eqtrd 2778 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
((-1↑((𝑁 + 1) −
1)) · ((𝑁 −
1)C((𝑁 + 1) − 1))) =
0) |
84 | 83 | oveq2d 7293 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(Σ𝑗 ∈ (1...𝑁)((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) + ((-1↑((𝑁 + 1) − 1)) · ((𝑁 − 1)C((𝑁 + 1) − 1)))) = (Σ𝑗 ∈ (1...𝑁)((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) + 0)) |
85 | | oveq1 7284 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝑘 → (𝑗 − 1) = (𝑘 − 1)) |
86 | 85 | oveq2d 7293 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑘 → (-1↑(𝑗 − 1)) = (-1↑(𝑘 − 1))) |
87 | 85 | oveq2d 7293 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑘 → ((𝑁 − 1)C(𝑗 − 1)) = ((𝑁 − 1)C(𝑘 − 1))) |
88 | 86, 87 | oveq12d 7295 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑘 → ((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = ((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) |
89 | 88 | cbvsumv 15406 |
. . . . . . . . 9
⊢
Σ𝑗 ∈
(1...𝑁)((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) |
90 | 89 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ (1...𝑁)((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) |
91 | 90 | oveq1d 7292 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
(Σ𝑗 ∈ (1...𝑁)((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) + 0) = (Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) + 0)) |
92 | | fzfid 13691 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(1...𝑁) ∈
Fin) |
93 | 26 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → -1 ∈
ℂ) |
94 | | elfznn 13283 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℕ) |
95 | | nnm1nn0 12272 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → (𝑘 − 1) ∈
ℕ0) |
96 | 94, 95 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...𝑁) → (𝑘 − 1) ∈
ℕ0) |
97 | 96 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (𝑘 − 1) ∈
ℕ0) |
98 | 93, 97 | expcld 13862 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (-1↑(𝑘 − 1)) ∈ ℂ) |
99 | | elfzelz 13254 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℤ) |
100 | | elfzel1 13253 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1...𝑁) → 1 ∈ ℤ) |
101 | 99, 100 | zsubcld 12429 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...𝑁) → (𝑘 − 1) ∈ ℤ) |
102 | 13, 101, 19 | syl2an 596 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((𝑁 − 1)C(𝑘 − 1)) ∈
ℕ0) |
103 | 102 | nn0cnd 12293 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℂ) |
104 | 98, 103 | mulcld 10993 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) ∈
ℂ) |
105 | 92, 104 | fsumcl 15443 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) ∈
ℂ) |
106 | 105 | addid1d 11173 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
(Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) + 0) = Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) |
107 | 91, 106 | eqtrd 2778 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
(Σ𝑗 ∈ (1...𝑁)((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) + 0) = Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) |
108 | 66, 84, 107 | 3eqtrd 2782 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ (1...(𝑁 + 1))((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) |
109 | 42, 46, 108 | 3eqtrd 2782 |
. . . 4
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · ((𝑁 − 1)C𝑘)) = Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) |
110 | | elnn0uz 12621 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
↔ 𝑁 ∈
(ℤ≥‘0)) |
111 | 70, 110 | sylib 217 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
(ℤ≥‘0)) |
112 | | oveq2 7285 |
. . . . . . 7
⊢ (𝑘 = 0 → (-1↑𝑘) =
(-1↑0)) |
113 | | oveq1 7284 |
. . . . . . . 8
⊢ (𝑘 = 0 → (𝑘 − 1) = (0 − 1)) |
114 | 113 | oveq2d 7293 |
. . . . . . 7
⊢ (𝑘 = 0 → ((𝑁 − 1)C(𝑘 − 1)) = ((𝑁 − 1)C(0 − 1))) |
115 | 112, 114 | oveq12d 7295 |
. . . . . 6
⊢ (𝑘 = 0 → ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = ((-1↑0) · ((𝑁 − 1)C(0 −
1)))) |
116 | 111, 34, 115 | fsum1p 15463 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = (((-1↑0) ·
((𝑁 − 1)C(0 −
1))) + Σ𝑘 ∈ ((0
+ 1)...𝑁)((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))))) |
117 | 27 | exp0d 13856 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(-1↑0) = 1) |
118 | | 0z 12328 |
. . . . . . . . . . 11
⊢ 0 ∈
ℤ |
119 | | zsubcl 12360 |
. . . . . . . . . . 11
⊢ ((0
∈ ℤ ∧ 1 ∈ ℤ) → (0 − 1) ∈
ℤ) |
120 | 118, 30, 119 | mp2an 689 |
. . . . . . . . . 10
⊢ (0
− 1) ∈ ℤ |
121 | 120 | a1i 11 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (0
− 1) ∈ ℤ) |
122 | | 0re 10975 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
123 | | ltm1 11815 |
. . . . . . . . . . 11
⊢ (0 ∈
ℝ → (0 − 1) < 0) |
124 | 122, 123 | mp1i 13 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (0
− 1) < 0) |
125 | 124 | orcd 870 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → ((0
− 1) < 0 ∨ (𝑁
− 1) < (0 − 1))) |
126 | | bcval4 14019 |
. . . . . . . . 9
⊢ (((𝑁 − 1) ∈
ℕ0 ∧ (0 − 1) ∈ ℤ ∧ ((0 − 1)
< 0 ∨ (𝑁 − 1)
< (0 − 1))) → ((𝑁 − 1)C(0 − 1)) =
0) |
127 | 13, 121, 125, 126 | syl3anc 1370 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1)C(0 − 1)) =
0) |
128 | 117, 127 | oveq12d 7295 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
((-1↑0) · ((𝑁
− 1)C(0 − 1))) = (1 · 0)) |
129 | 6 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 1 ∈
ℂ) |
130 | 129 | mul01d 11172 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (1
· 0) = 0) |
131 | 128, 130 | eqtrd 2778 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
((-1↑0) · ((𝑁
− 1)C(0 − 1))) = 0) |
132 | 43 | a1i 11 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (0 + 1) =
1) |
133 | 132 | oveq1d 7292 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((0 +
1)...𝑁) = (1...𝑁)) |
134 | 99 | zcnd 12425 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℂ) |
135 | | npcan1 11398 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℂ → ((𝑘 − 1) + 1) = 𝑘) |
136 | 135 | eqcomd 2744 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℂ → 𝑘 = ((𝑘 − 1) + 1)) |
137 | 134, 136 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1...𝑁) → 𝑘 = ((𝑘 − 1) + 1)) |
138 | 137 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → 𝑘 = ((𝑘 − 1) + 1)) |
139 | 138 | oveq2d 7293 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (-1↑𝑘) = (-1↑((𝑘 − 1) + 1))) |
140 | | expp1 13787 |
. . . . . . . . . . . 12
⊢ ((-1
∈ ℂ ∧ (𝑘
− 1) ∈ ℕ0) → (-1↑((𝑘 − 1) + 1)) = ((-1↑(𝑘 − 1)) ·
-1)) |
141 | 27, 96, 140 | syl2an 596 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (-1↑((𝑘 − 1) + 1)) = ((-1↑(𝑘 − 1)) ·
-1)) |
142 | 139, 141 | eqtrd 2778 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (-1↑𝑘) = ((-1↑(𝑘 − 1)) · -1)) |
143 | 142 | oveq1d 7292 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = (((-1↑(𝑘 − 1)) · -1)
· ((𝑁 −
1)C(𝑘 −
1)))) |
144 | 98, 93 | mulcomd 10994 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((-1↑(𝑘 − 1)) · -1) = (-1 ·
(-1↑(𝑘 −
1)))) |
145 | 144 | oveq1d 7292 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (((-1↑(𝑘 − 1)) · -1) · ((𝑁 − 1)C(𝑘 − 1))) = ((-1 · (-1↑(𝑘 − 1))) · ((𝑁 − 1)C(𝑘 − 1)))) |
146 | 93, 98, 103 | mulassd 10996 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((-1 · (-1↑(𝑘 − 1))) · ((𝑁 − 1)C(𝑘 − 1))) = (-1 · ((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))) |
147 | 143, 145,
146 | 3eqtrd 2782 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = (-1 · ((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))) |
148 | 133, 147 | sumeq12rdv 15417 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ ((0 +
1)...𝑁)((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = Σ𝑘 ∈ (1...𝑁)(-1 · ((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))) |
149 | 92, 27, 104 | fsummulc2 15494 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → (-1
· Σ𝑘 ∈
(1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) = Σ𝑘 ∈ (1...𝑁)(-1 · ((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))) |
150 | 148, 149 | eqtr4d 2781 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ ((0 +
1)...𝑁)((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))) |
151 | 131, 150 | oveq12d 7295 |
. . . . 5
⊢ (𝑁 ∈ ℕ →
(((-1↑0) · ((𝑁
− 1)C(0 − 1))) + Σ𝑘 ∈ ((0 + 1)...𝑁)((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1)))) = (0 + (-1 ·
Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))))) |
152 | 27, 105 | mulcld 10993 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (-1
· Σ𝑘 ∈
(1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) ∈
ℂ) |
153 | 152 | addid2d 11174 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (0 + (-1
· Σ𝑘 ∈
(1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))) = (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))) |
154 | 116, 151,
153 | 3eqtrd 2782 |
. . . 4
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))) |
155 | 109, 154 | oveq12d 7295 |
. . 3
⊢ (𝑁 ∈ ℕ →
(Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · ((𝑁 − 1)C𝑘)) + Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1)))) = (Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) + (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))))) |
156 | 35, 155 | eqtrd 2778 |
. 2
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ (0...𝑁)(((-1↑𝑘) · ((𝑁 − 1)C𝑘)) + ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1)))) = (Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) + (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))))) |
157 | 105 | mulm1d 11425 |
. . . 4
⊢ (𝑁 ∈ ℕ → (-1
· Σ𝑘 ∈
(1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) = -Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) |
158 | 157 | oveq2d 7293 |
. . 3
⊢ (𝑁 ∈ ℕ →
(Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) + (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))) = (Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) + -Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))) |
159 | 105 | negidd 11320 |
. . 3
⊢ (𝑁 ∈ ℕ →
(Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) + -Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) = 0) |
160 | 158, 159 | eqtrd 2778 |
. 2
⊢ (𝑁 ∈ ℕ →
(Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) + (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))) = 0) |
161 | 24, 156, 160 | 3eqtrd 2782 |
1
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · (𝑁C𝑘)) = 0) |