| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elfzelz 13565 | . . . . . . 7
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℤ) | 
| 2 |  | bcpascm1 48272 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ) → (((𝑁 − 1)C𝑘) + ((𝑁 − 1)C(𝑘 − 1))) = (𝑁C𝑘)) | 
| 3 | 1, 2 | sylan2 593 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → (((𝑁 − 1)C𝑘) + ((𝑁 − 1)C(𝑘 − 1))) = (𝑁C𝑘)) | 
| 4 | 3 | eqcomd 2742 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → (𝑁C𝑘) = (((𝑁 − 1)C𝑘) + ((𝑁 − 1)C(𝑘 − 1)))) | 
| 5 | 4 | oveq2d 7448 | . . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((-1↑𝑘) · (𝑁C𝑘)) = ((-1↑𝑘) · (((𝑁 − 1)C𝑘) + ((𝑁 − 1)C(𝑘 − 1))))) | 
| 6 |  | ax-1cn 11214 | . . . . . . 7
⊢ 1 ∈
ℂ | 
| 7 |  | negcl 11509 | . . . . . . . 8
⊢ (1 ∈
ℂ → -1 ∈ ℂ) | 
| 8 |  | elfznn0 13661 | . . . . . . . 8
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) | 
| 9 |  | expcl 14121 | . . . . . . . 8
⊢ ((-1
∈ ℂ ∧ 𝑘
∈ ℕ0) → (-1↑𝑘) ∈ ℂ) | 
| 10 | 7, 8, 9 | syl2an 596 | . . . . . . 7
⊢ ((1
∈ ℂ ∧ 𝑘
∈ (0...𝑁)) →
(-1↑𝑘) ∈
ℂ) | 
| 11 | 6, 10 | mpan 690 | . . . . . 6
⊢ (𝑘 ∈ (0...𝑁) → (-1↑𝑘) ∈ ℂ) | 
| 12 | 11 | adantl 481 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → (-1↑𝑘) ∈ ℂ) | 
| 13 |  | nnm1nn0 12569 | . . . . . 6
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) | 
| 14 |  | bccl 14362 | . . . . . . 7
⊢ (((𝑁 − 1) ∈
ℕ0 ∧ 𝑘
∈ ℤ) → ((𝑁
− 1)C𝑘) ∈
ℕ0) | 
| 15 | 14 | nn0cnd 12591 | . . . . . 6
⊢ (((𝑁 − 1) ∈
ℕ0 ∧ 𝑘
∈ ℤ) → ((𝑁
− 1)C𝑘) ∈
ℂ) | 
| 16 | 13, 1, 15 | syl2an 596 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁 − 1)C𝑘) ∈ ℂ) | 
| 17 |  | peano2zm 12662 | . . . . . . 7
⊢ (𝑘 ∈ ℤ → (𝑘 − 1) ∈
ℤ) | 
| 18 | 1, 17 | syl 17 | . . . . . 6
⊢ (𝑘 ∈ (0...𝑁) → (𝑘 − 1) ∈ ℤ) | 
| 19 |  | bccl 14362 | . . . . . . 7
⊢ (((𝑁 − 1) ∈
ℕ0 ∧ (𝑘 − 1) ∈ ℤ) → ((𝑁 − 1)C(𝑘 − 1)) ∈
ℕ0) | 
| 20 | 19 | nn0cnd 12591 | . . . . . 6
⊢ (((𝑁 − 1) ∈
ℕ0 ∧ (𝑘 − 1) ∈ ℤ) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℂ) | 
| 21 | 13, 18, 20 | syl2an 596 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℂ) | 
| 22 | 12, 16, 21 | adddid 11286 | . . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((-1↑𝑘) · (((𝑁 − 1)C𝑘) + ((𝑁 − 1)C(𝑘 − 1)))) = (((-1↑𝑘) · ((𝑁 − 1)C𝑘)) + ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))))) | 
| 23 | 5, 22 | eqtrd 2776 | . . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((-1↑𝑘) · (𝑁C𝑘)) = (((-1↑𝑘) · ((𝑁 − 1)C𝑘)) + ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))))) | 
| 24 | 23 | sumeq2dv 15739 | . 2
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · (𝑁C𝑘)) = Σ𝑘 ∈ (0...𝑁)(((-1↑𝑘) · ((𝑁 − 1)C𝑘)) + ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))))) | 
| 25 |  | fzfid 14015 | . . . 4
⊢ (𝑁 ∈ ℕ →
(0...𝑁) ∈
Fin) | 
| 26 |  | neg1cn 12381 | . . . . . . 7
⊢ -1 ∈
ℂ | 
| 27 | 26 | a1i 11 | . . . . . 6
⊢ (𝑁 ∈ ℕ → -1 ∈
ℂ) | 
| 28 | 27, 8, 9 | syl2an 596 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → (-1↑𝑘) ∈ ℂ) | 
| 29 | 28, 16 | mulcld 11282 | . . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((-1↑𝑘) · ((𝑁 − 1)C𝑘)) ∈ ℂ) | 
| 30 |  | 1z 12649 | . . . . . . . 8
⊢ 1 ∈
ℤ | 
| 31 | 30 | a1i 11 | . . . . . . 7
⊢ (𝑘 ∈ (0...𝑁) → 1 ∈ ℤ) | 
| 32 | 1, 31 | zsubcld 12729 | . . . . . 6
⊢ (𝑘 ∈ (0...𝑁) → (𝑘 − 1) ∈ ℤ) | 
| 33 | 13, 32, 20 | syl2an 596 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℂ) | 
| 34 | 28, 33 | mulcld 11282 | . . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) ∈
ℂ) | 
| 35 | 25, 29, 34 | fsumadd 15777 | . . 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 12627 | . . . . . 6
⊢ (𝑁 ∈ ℕ → 0 ∈
ℤ) | 
| 38 |  | nnz 12636 | . . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) | 
| 39 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑘 = (𝑗 − 1) → (-1↑𝑘) = (-1↑(𝑗 − 1))) | 
| 40 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑘 = (𝑗 − 1) → ((𝑁 − 1)C𝑘) = ((𝑁 − 1)C(𝑗 − 1))) | 
| 41 | 39, 40 | oveq12d 7450 | . . . . . 6
⊢ (𝑘 = (𝑗 − 1) → ((-1↑𝑘) · ((𝑁 − 1)C𝑘)) = ((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1)))) | 
| 42 | 36, 37, 38, 29, 41 | fsumshft 15817 | . . . . 5
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · ((𝑁 − 1)C𝑘)) = Σ𝑗 ∈ ((0 + 1)...(𝑁 + 1))((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1)))) | 
| 43 |  | 0p1e1 12389 | . . . . . . . 8
⊢ (0 + 1) =
1 | 
| 44 | 43 | oveq1i 7442 | . . . . . . 7
⊢ ((0 +
1)...(𝑁 + 1)) = (1...(𝑁 + 1)) | 
| 45 | 44 | a1i 11 | . . . . . 6
⊢ (𝑁 ∈ ℕ → ((0 +
1)...(𝑁 + 1)) = (1...(𝑁 + 1))) | 
| 46 | 45 | sumeq1d 15737 | . . . . 5
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ ((0 +
1)...(𝑁 +
1))((-1↑(𝑗 − 1))
· ((𝑁 −
1)C(𝑗 − 1))) =
Σ𝑗 ∈ (1...(𝑁 + 1))((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1)))) | 
| 47 |  | elnnuz 12923 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈
(ℤ≥‘1)) | 
| 48 | 47 | biimpi 216 | . . . . . . 7
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
(ℤ≥‘1)) | 
| 49 | 26 | a1i 11 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → -1 ∈
ℂ) | 
| 50 |  | elfznn 13594 | . . . . . . . . . . 11
⊢ (𝑗 ∈ (1...(𝑁 + 1)) → 𝑗 ∈ ℕ) | 
| 51 |  | nnm1nn0 12569 | . . . . . . . . . . 11
⊢ (𝑗 ∈ ℕ → (𝑗 − 1) ∈
ℕ0) | 
| 52 | 50, 51 | syl 17 | . . . . . . . . . 10
⊢ (𝑗 ∈ (1...(𝑁 + 1)) → (𝑗 − 1) ∈
ℕ0) | 
| 53 | 52 | adantl 481 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → (𝑗 − 1) ∈
ℕ0) | 
| 54 | 49, 53 | expcld 14187 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → (-1↑(𝑗 − 1)) ∈ ℂ) | 
| 55 |  | elfzelz 13565 | . . . . . . . . . 10
⊢ (𝑗 ∈ (1...(𝑁 + 1)) → 𝑗 ∈ ℤ) | 
| 56 |  | elfzel1 13564 | . . . . . . . . . 10
⊢ (𝑗 ∈ (1...(𝑁 + 1)) → 1 ∈
ℤ) | 
| 57 | 55, 56 | zsubcld 12729 | . . . . . . . . 9
⊢ (𝑗 ∈ (1...(𝑁 + 1)) → (𝑗 − 1) ∈ ℤ) | 
| 58 |  | bccl 14362 | . . . . . . . . . 10
⊢ (((𝑁 − 1) ∈
ℕ0 ∧ (𝑗 − 1) ∈ ℤ) → ((𝑁 − 1)C(𝑗 − 1)) ∈
ℕ0) | 
| 59 | 58 | nn0cnd 12591 | . . . . . . . . 9
⊢ (((𝑁 − 1) ∈
ℕ0 ∧ (𝑗 − 1) ∈ ℤ) → ((𝑁 − 1)C(𝑗 − 1)) ∈ ℂ) | 
| 60 | 13, 57, 59 | syl2an 596 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → ((𝑁 − 1)C(𝑗 − 1)) ∈ ℂ) | 
| 61 | 54, 60 | mulcld 11282 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → ((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) ∈
ℂ) | 
| 62 |  | oveq1 7439 | . . . . . . . . 9
⊢ (𝑗 = (𝑁 + 1) → (𝑗 − 1) = ((𝑁 + 1) − 1)) | 
| 63 | 62 | oveq2d 7448 | . . . . . . . 8
⊢ (𝑗 = (𝑁 + 1) → (-1↑(𝑗 − 1)) = (-1↑((𝑁 + 1) − 1))) | 
| 64 | 62 | oveq2d 7448 | . . . . . . . 8
⊢ (𝑗 = (𝑁 + 1) → ((𝑁 − 1)C(𝑗 − 1)) = ((𝑁 − 1)C((𝑁 + 1) − 1))) | 
| 65 | 63, 64 | oveq12d 7450 | . . . . . . 7
⊢ (𝑗 = (𝑁 + 1) → ((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = ((-1↑((𝑁 + 1) − 1)) · ((𝑁 − 1)C((𝑁 + 1) − 1)))) | 
| 66 | 48, 61, 65 | fsump1 15793 | . . . . . 6
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ (1...(𝑁 + 1))((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = (Σ𝑗 ∈ (1...𝑁)((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) + ((-1↑((𝑁 + 1) − 1)) · ((𝑁 − 1)C((𝑁 + 1) − 1))))) | 
| 67 |  | nncn 12275 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) | 
| 68 |  | pncan1 11688 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁) | 
| 69 | 67, 68 | syl 17 | . . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = 𝑁) | 
| 70 |  | nnnn0 12535 | . . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) | 
| 71 | 69, 70 | eqeltrd 2840 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) ∈
ℕ0) | 
| 72 | 71 | nn0zd 12641 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) ∈
ℤ) | 
| 73 |  | nnre 12274 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) | 
| 74 |  | ltm1 12110 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℝ → (𝑁 − 1) < 𝑁) | 
| 75 | 73, 74 | syl 17 | . . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) < 𝑁) | 
| 76 | 75, 69 | breqtrrd 5170 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) < ((𝑁 + 1) −
1)) | 
| 77 | 76 | olcd 874 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) − 1) < 0 ∨
(𝑁 − 1) < ((𝑁 + 1) −
1))) | 
| 78 |  | bcval4 14347 | . . . . . . . . . 10
⊢ (((𝑁 − 1) ∈
ℕ0 ∧ ((𝑁 + 1) − 1) ∈ ℤ ∧
(((𝑁 + 1) − 1) < 0
∨ (𝑁 − 1) <
((𝑁 + 1) − 1)))
→ ((𝑁 −
1)C((𝑁 + 1) − 1)) =
0) | 
| 79 | 13, 72, 77, 78 | syl3anc 1372 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1)C((𝑁 + 1) − 1)) = 0) | 
| 80 | 79 | oveq2d 7448 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ →
((-1↑((𝑁 + 1) −
1)) · ((𝑁 −
1)C((𝑁 + 1) − 1))) =
((-1↑((𝑁 + 1) −
1)) · 0)) | 
| 81 | 27, 71 | expcld 14187 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(-1↑((𝑁 + 1) −
1)) ∈ ℂ) | 
| 82 | 81 | mul01d 11461 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ →
((-1↑((𝑁 + 1) −
1)) · 0) = 0) | 
| 83 | 80, 82 | eqtrd 2776 | . . . . . . 7
⊢ (𝑁 ∈ ℕ →
((-1↑((𝑁 + 1) −
1)) · ((𝑁 −
1)C((𝑁 + 1) − 1))) =
0) | 
| 84 | 83 | oveq2d 7448 | . . . . . 6
⊢ (𝑁 ∈ ℕ →
(Σ𝑗 ∈ (1...𝑁)((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) + ((-1↑((𝑁 + 1) − 1)) · ((𝑁 − 1)C((𝑁 + 1) − 1)))) = (Σ𝑗 ∈ (1...𝑁)((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) + 0)) | 
| 85 |  | oveq1 7439 | . . . . . . . . . . . 12
⊢ (𝑗 = 𝑘 → (𝑗 − 1) = (𝑘 − 1)) | 
| 86 | 85 | oveq2d 7448 | . . . . . . . . . . 11
⊢ (𝑗 = 𝑘 → (-1↑(𝑗 − 1)) = (-1↑(𝑘 − 1))) | 
| 87 | 85 | oveq2d 7448 | . . . . . . . . . . 11
⊢ (𝑗 = 𝑘 → ((𝑁 − 1)C(𝑗 − 1)) = ((𝑁 − 1)C(𝑘 − 1))) | 
| 88 | 86, 87 | oveq12d 7450 | . . . . . . . . . 10
⊢ (𝑗 = 𝑘 → ((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = ((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) | 
| 89 | 88 | cbvsumv 15733 | . . . . . . . . 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 7447 | . . . . . . 7
⊢ (𝑁 ∈ ℕ →
(Σ𝑗 ∈ (1...𝑁)((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) + 0) = (Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) + 0)) | 
| 92 |  | fzfid 14015 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(1...𝑁) ∈
Fin) | 
| 93 | 26 | a1i 11 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → -1 ∈
ℂ) | 
| 94 |  | elfznn 13594 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℕ) | 
| 95 |  | nnm1nn0 12569 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → (𝑘 − 1) ∈
ℕ0) | 
| 96 | 94, 95 | syl 17 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...𝑁) → (𝑘 − 1) ∈
ℕ0) | 
| 97 | 96 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (𝑘 − 1) ∈
ℕ0) | 
| 98 | 93, 97 | expcld 14187 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (-1↑(𝑘 − 1)) ∈ ℂ) | 
| 99 |  | elfzelz 13565 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℤ) | 
| 100 |  | elfzel1 13564 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1...𝑁) → 1 ∈ ℤ) | 
| 101 | 99, 100 | zsubcld 12729 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ (1...𝑁) → (𝑘 − 1) ∈ ℤ) | 
| 102 | 13, 101, 19 | syl2an 596 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((𝑁 − 1)C(𝑘 − 1)) ∈
ℕ0) | 
| 103 | 102 | nn0cnd 12591 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℂ) | 
| 104 | 98, 103 | mulcld 11282 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) ∈
ℂ) | 
| 105 | 92, 104 | fsumcl 15770 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) ∈
ℂ) | 
| 106 | 105 | addridd 11462 | . . . . . . 7
⊢ (𝑁 ∈ ℕ →
(Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) + 0) = Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) | 
| 107 | 91, 106 | eqtrd 2776 | . . . . . 6
⊢ (𝑁 ∈ ℕ →
(Σ𝑗 ∈ (1...𝑁)((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) + 0) = Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) | 
| 108 | 66, 84, 107 | 3eqtrd 2780 | . . . . 5
⊢ (𝑁 ∈ ℕ →
Σ𝑗 ∈ (1...(𝑁 + 1))((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) | 
| 109 | 42, 46, 108 | 3eqtrd 2780 | . . . 4
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · ((𝑁 − 1)C𝑘)) = Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) | 
| 110 |  | elnn0uz 12924 | . . . . . . 7
⊢ (𝑁 ∈ ℕ0
↔ 𝑁 ∈
(ℤ≥‘0)) | 
| 111 | 70, 110 | sylib 218 | . . . . . 6
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
(ℤ≥‘0)) | 
| 112 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑘 = 0 → (-1↑𝑘) =
(-1↑0)) | 
| 113 |  | oveq1 7439 | . . . . . . . 8
⊢ (𝑘 = 0 → (𝑘 − 1) = (0 − 1)) | 
| 114 | 113 | oveq2d 7448 | . . . . . . 7
⊢ (𝑘 = 0 → ((𝑁 − 1)C(𝑘 − 1)) = ((𝑁 − 1)C(0 − 1))) | 
| 115 | 112, 114 | oveq12d 7450 | . . . . . 6
⊢ (𝑘 = 0 → ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = ((-1↑0) · ((𝑁 − 1)C(0 −
1)))) | 
| 116 | 111, 34, 115 | fsum1p 15790 | . . . . 5
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = (((-1↑0) ·
((𝑁 − 1)C(0 −
1))) + Σ𝑘 ∈ ((0
+ 1)...𝑁)((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))))) | 
| 117 | 27 | exp0d 14181 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(-1↑0) = 1) | 
| 118 |  | 0z 12626 | . . . . . . . . . . 11
⊢ 0 ∈
ℤ | 
| 119 |  | zsubcl 12661 | . . . . . . . . . . 11
⊢ ((0
∈ ℤ ∧ 1 ∈ ℤ) → (0 − 1) ∈
ℤ) | 
| 120 | 118, 30, 119 | mp2an 692 | . . . . . . . . . 10
⊢ (0
− 1) ∈ ℤ | 
| 121 | 120 | a1i 11 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (0
− 1) ∈ ℤ) | 
| 122 |  | 0re 11264 | . . . . . . . . . . 11
⊢ 0 ∈
ℝ | 
| 123 |  | ltm1 12110 | . . . . . . . . . . 11
⊢ (0 ∈
ℝ → (0 − 1) < 0) | 
| 124 | 122, 123 | mp1i 13 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (0
− 1) < 0) | 
| 125 | 124 | orcd 873 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ → ((0
− 1) < 0 ∨ (𝑁
− 1) < (0 − 1))) | 
| 126 |  | bcval4 14347 | . . . . . . . . 9
⊢ (((𝑁 − 1) ∈
ℕ0 ∧ (0 − 1) ∈ ℤ ∧ ((0 − 1)
< 0 ∨ (𝑁 − 1)
< (0 − 1))) → ((𝑁 − 1)C(0 − 1)) =
0) | 
| 127 | 13, 121, 125, 126 | syl3anc 1372 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1)C(0 − 1)) =
0) | 
| 128 | 117, 127 | oveq12d 7450 | . . . . . . 7
⊢ (𝑁 ∈ ℕ →
((-1↑0) · ((𝑁
− 1)C(0 − 1))) = (1 · 0)) | 
| 129 | 6 | a1i 11 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ → 1 ∈
ℂ) | 
| 130 | 129 | mul01d 11461 | . . . . . . 7
⊢ (𝑁 ∈ ℕ → (1
· 0) = 0) | 
| 131 | 128, 130 | eqtrd 2776 | . . . . . 6
⊢ (𝑁 ∈ ℕ →
((-1↑0) · ((𝑁
− 1)C(0 − 1))) = 0) | 
| 132 | 43 | a1i 11 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (0 + 1) =
1) | 
| 133 | 132 | oveq1d 7447 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ → ((0 +
1)...𝑁) = (1...𝑁)) | 
| 134 | 99 | zcnd 12725 | . . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℂ) | 
| 135 |  | npcan1 11689 | . . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℂ → ((𝑘 − 1) + 1) = 𝑘) | 
| 136 | 135 | eqcomd 2742 | . . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℂ → 𝑘 = ((𝑘 − 1) + 1)) | 
| 137 | 134, 136 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1...𝑁) → 𝑘 = ((𝑘 − 1) + 1)) | 
| 138 | 137 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → 𝑘 = ((𝑘 − 1) + 1)) | 
| 139 | 138 | oveq2d 7448 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (-1↑𝑘) = (-1↑((𝑘 − 1) + 1))) | 
| 140 |  | expp1 14110 | . . . . . . . . . . . 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 2776 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (-1↑𝑘) = ((-1↑(𝑘 − 1)) · -1)) | 
| 143 | 142 | oveq1d 7447 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = (((-1↑(𝑘 − 1)) · -1)
· ((𝑁 −
1)C(𝑘 −
1)))) | 
| 144 | 98, 93 | mulcomd 11283 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((-1↑(𝑘 − 1)) · -1) = (-1 ·
(-1↑(𝑘 −
1)))) | 
| 145 | 144 | oveq1d 7447 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (((-1↑(𝑘 − 1)) · -1) · ((𝑁 − 1)C(𝑘 − 1))) = ((-1 · (-1↑(𝑘 − 1))) · ((𝑁 − 1)C(𝑘 − 1)))) | 
| 146 | 93, 98, 103 | mulassd 11285 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((-1 · (-1↑(𝑘 − 1))) · ((𝑁 − 1)C(𝑘 − 1))) = (-1 · ((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))) | 
| 147 | 143, 145,
146 | 3eqtrd 2780 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = (-1 · ((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))) | 
| 148 | 133, 147 | sumeq12rdv 15744 | . . . . . . 7
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ ((0 +
1)...𝑁)((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = Σ𝑘 ∈ (1...𝑁)(-1 · ((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))) | 
| 149 | 92, 27, 104 | fsummulc2 15821 | . . . . . . 7
⊢ (𝑁 ∈ ℕ → (-1
· Σ𝑘 ∈
(1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) = Σ𝑘 ∈ (1...𝑁)(-1 · ((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))) | 
| 150 | 148, 149 | eqtr4d 2779 | . . . . . 6
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ ((0 +
1)...𝑁)((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))) | 
| 151 | 131, 150 | oveq12d 7450 | . . . . 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 11282 | . . . . . 6
⊢ (𝑁 ∈ ℕ → (-1
· Σ𝑘 ∈
(1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) ∈
ℂ) | 
| 153 | 152 | addlidd 11463 | . . . . 5
⊢ (𝑁 ∈ ℕ → (0 + (-1
· Σ𝑘 ∈
(1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))) = (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))) | 
| 154 | 116, 151,
153 | 3eqtrd 2780 | . . . 4
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))) | 
| 155 | 109, 154 | oveq12d 7450 | . . 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 2776 | . 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 11716 | . . . 4
⊢ (𝑁 ∈ ℕ → (-1
· Σ𝑘 ∈
(1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) = -Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) | 
| 158 | 157 | oveq2d 7448 | . . 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 11611 | . . 3
⊢ (𝑁 ∈ ℕ →
(Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) + -Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) = 0) | 
| 160 | 158, 159 | eqtrd 2776 | . 2
⊢ (𝑁 ∈ ℕ →
(Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) + (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))) = 0) | 
| 161 | 24, 156, 160 | 3eqtrd 2780 | 1
⊢ (𝑁 ∈ ℕ →
Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · (𝑁C𝑘)) = 0) |