Metamath Proof Explorer

Theorem altgsumbcALT

Description: Alternate proof of altgsumbc , using Pascal's rule ( bcpascm1 ) instead of the binomial theorem ( binom ). (Contributed by AV, 8-Sep-2019) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion altgsumbcALT ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( - 1 ↑ 𝑘 ) · ( 𝑁 C 𝑘 ) ) = 0 )

Proof

Step Hyp Ref Expression
1 elfzelz ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℤ )
2 bcpascm1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ ) → ( ( ( 𝑁 − 1 ) C 𝑘 ) + ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) = ( 𝑁 C 𝑘 ) )
3 1 2 sylan2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑁 − 1 ) C 𝑘 ) + ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) = ( 𝑁 C 𝑘 ) )
4 3 eqcomd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝑘 ) = ( ( ( 𝑁 − 1 ) C 𝑘 ) + ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) )
5 4 oveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( - 1 ↑ 𝑘 ) · ( 𝑁 C 𝑘 ) ) = ( ( - 1 ↑ 𝑘 ) · ( ( ( 𝑁 − 1 ) C 𝑘 ) + ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) ) )
6 ax-1cn ⊢ 1 ∈ ℂ
7 negcl ⊢ ( 1 ∈ ℂ → - 1 ∈ ℂ )
8 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
9 expcl ⊢ ( ( - 1 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( - 1 ↑ 𝑘 ) ∈ ℂ )
10 7 8 9 syl2an ⊢ ( ( 1 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( - 1 ↑ 𝑘 ) ∈ ℂ )
11 6 10 mpan ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( - 1 ↑ 𝑘 ) ∈ ℂ )
12 11 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( - 1 ↑ 𝑘 ) ∈ ℂ )
13 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
14 bccl ⊢ ( ( ( 𝑁 − 1 ) ∈ ℕ0 ∧ 𝑘 ∈ ℤ ) → ( ( 𝑁 − 1 ) C 𝑘 ) ∈ ℕ0 )
15 14 nn0cnd ⊢ ( ( ( 𝑁 − 1 ) ∈ ℕ0 ∧ 𝑘 ∈ ℤ ) → ( ( 𝑁 − 1 ) C 𝑘 ) ∈ ℂ )
16 13 1 15 syl2an ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 1 ) C 𝑘 ) ∈ ℂ )
17 peano2zm ⊢ ( 𝑘 ∈ ℤ → ( 𝑘 − 1 ) ∈ ℤ )
18 1 17 syl ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( 𝑘 − 1 ) ∈ ℤ )
19 bccl ⊢ ( ( ( 𝑁 − 1 ) ∈ ℕ0 ∧ ( 𝑘 − 1 ) ∈ ℤ ) → ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ∈ ℕ0 )
20 19 nn0cnd ⊢ ( ( ( 𝑁 − 1 ) ∈ ℕ0 ∧ ( 𝑘 − 1 ) ∈ ℤ ) → ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ∈ ℂ )
21 13 18 20 syl2an ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ∈ ℂ )
22 12 16 21 adddid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( - 1 ↑ 𝑘 ) · ( ( ( 𝑁 − 1 ) C 𝑘 ) + ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) ) = ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 1 ) C 𝑘 ) ) + ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) ) )
23 5 22 eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( - 1 ↑ 𝑘 ) · ( 𝑁 C 𝑘 ) ) = ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 1 ) C 𝑘 ) ) + ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) ) )
24 23 sumeq2dv ⊢ ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( - 1 ↑ 𝑘 ) · ( 𝑁 C 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 1 ) C 𝑘 ) ) + ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) ) )
25 fzfid ⊢ ( 𝑁 ∈ ℕ → ( 0 ... 𝑁 ) ∈ Fin )
26 neg1cn ⊢ - 1 ∈ ℂ
27 26 a1i ⊢ ( 𝑁 ∈ ℕ → - 1 ∈ ℂ )
28 27 8 9 syl2an ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( - 1 ↑ 𝑘 ) ∈ ℂ )
29 28 16 mulcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 1 ) C 𝑘 ) ) ∈ ℂ )
30 1z ⊢ 1 ∈ ℤ
31 30 a1i ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 1 ∈ ℤ )
32 1 31 zsubcld ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( 𝑘 − 1 ) ∈ ℤ )
33 13 32 20 syl2an ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ∈ ℂ )
34 28 33 mulcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) ∈ ℂ )
35 25 29 34 fsumadd ⊢ ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 1 ) C 𝑘 ) ) + ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) ) = ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 1 ) C 𝑘 ) ) + Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) ) )
36 30 a1i ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℤ )
37 0zd ⊢ ( 𝑁 ∈ ℕ → 0 ∈ ℤ )
38 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
39 oveq2 ⊢ ( 𝑘 = ( 𝑗 − 1 ) → ( - 1 ↑ 𝑘 ) = ( - 1 ↑ ( 𝑗 − 1 ) ) )
40 oveq2 ⊢ ( 𝑘 = ( 𝑗 − 1 ) → ( ( 𝑁 − 1 ) C 𝑘 ) = ( ( 𝑁 − 1 ) C ( 𝑗 − 1 ) ) )
41 39 40 oveq12d ⊢ ( 𝑘 = ( 𝑗 − 1 ) → ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 1 ) C 𝑘 ) ) = ( ( - 1 ↑ ( 𝑗 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑗 − 1 ) ) ) )
42 36 37 38 29 41 fsumshft ⊢ ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 1 ) C 𝑘 ) ) = Σ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ( ( - 1 ↑ ( 𝑗 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑗 − 1 ) ) ) )
43 0p1e1 ⊢ ( 0 + 1 ) = 1
44 43 oveq1i ⊢ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) = ( 1 ... ( 𝑁 + 1 ) )
45 44 a1i ⊢ ( 𝑁 ∈ ℕ → ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) = ( 1 ... ( 𝑁 + 1 ) ) )
46 45 sumeq1d ⊢ ( 𝑁 ∈ ℕ → Σ 𝑗 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ( ( - 1 ↑ ( 𝑗 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑗 − 1 ) ) ) = Σ 𝑗 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( ( - 1 ↑ ( 𝑗 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑗 − 1 ) ) ) )
47 elnnuz ⊢ ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
48 47 biimpi ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
49 26 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → - 1 ∈ ℂ )
50 elfznn ⊢ ( 𝑗 ∈ ( 1 ... ( 𝑁 + 1 ) ) → 𝑗 ∈ ℕ )
51 nnm1nn0 ⊢ ( 𝑗 ∈ ℕ → ( 𝑗 − 1 ) ∈ ℕ0 )
52 50 51 syl ⊢ ( 𝑗 ∈ ( 1 ... ( 𝑁 + 1 ) ) → ( 𝑗 − 1 ) ∈ ℕ0 )
53 52 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( 𝑗 − 1 ) ∈ ℕ0 )
54 49 53 expcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( - 1 ↑ ( 𝑗 − 1 ) ) ∈ ℂ )
55 elfzelz ⊢ ( 𝑗 ∈ ( 1 ... ( 𝑁 + 1 ) ) → 𝑗 ∈ ℤ )
56 elfzel1 ⊢ ( 𝑗 ∈ ( 1 ... ( 𝑁 + 1 ) ) → 1 ∈ ℤ )
57 55 56 zsubcld ⊢ ( 𝑗 ∈ ( 1 ... ( 𝑁 + 1 ) ) → ( 𝑗 − 1 ) ∈ ℤ )
58 bccl ⊢ ( ( ( 𝑁 − 1 ) ∈ ℕ0 ∧ ( 𝑗 − 1 ) ∈ ℤ ) → ( ( 𝑁 − 1 ) C ( 𝑗 − 1 ) ) ∈ ℕ0 )
59 58 nn0cnd ⊢ ( ( ( 𝑁 − 1 ) ∈ ℕ0 ∧ ( 𝑗 − 1 ) ∈ ℤ ) → ( ( 𝑁 − 1 ) C ( 𝑗 − 1 ) ) ∈ ℂ )
60 13 57 59 syl2an ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 − 1 ) C ( 𝑗 − 1 ) ) ∈ ℂ )
61 54 60 mulcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → ( ( - 1 ↑ ( 𝑗 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑗 − 1 ) ) ) ∈ ℂ )
62 oveq1 ⊢ ( 𝑗 = ( 𝑁 + 1 ) → ( 𝑗 − 1 ) = ( ( 𝑁 + 1 ) − 1 ) )
63 62 oveq2d ⊢ ( 𝑗 = ( 𝑁 + 1 ) → ( - 1 ↑ ( 𝑗 − 1 ) ) = ( - 1 ↑ ( ( 𝑁 + 1 ) − 1 ) ) )
64 62 oveq2d ⊢ ( 𝑗 = ( 𝑁 + 1 ) → ( ( 𝑁 − 1 ) C ( 𝑗 − 1 ) ) = ( ( 𝑁 − 1 ) C ( ( 𝑁 + 1 ) − 1 ) ) )
65 63 64 oveq12d ⊢ ( 𝑗 = ( 𝑁 + 1 ) → ( ( - 1 ↑ ( 𝑗 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑗 − 1 ) ) ) = ( ( - 1 ↑ ( ( 𝑁 + 1 ) − 1 ) ) · ( ( 𝑁 − 1 ) C ( ( 𝑁 + 1 ) − 1 ) ) ) )
66 48 61 65 fsump1 ⊢ ( 𝑁 ∈ ℕ → Σ 𝑗 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( ( - 1 ↑ ( 𝑗 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑗 − 1 ) ) ) = ( Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( - 1 ↑ ( 𝑗 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑗 − 1 ) ) ) + ( ( - 1 ↑ ( ( 𝑁 + 1 ) − 1 ) ) · ( ( 𝑁 − 1 ) C ( ( 𝑁 + 1 ) − 1 ) ) ) ) )
67 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
68 pncan1 ⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
69 67 68 syl ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
70 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
71 69 70 eqeltrd ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 + 1 ) − 1 ) ∈ ℕ0 )
72 71 nn0zd ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 + 1 ) − 1 ) ∈ ℤ )
73 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
74 ltm1 ⊢ ( 𝑁 ∈ ℝ → ( 𝑁 − 1 ) < 𝑁 )
75 73 74 syl ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) < 𝑁 )
76 75 69 breqtrrd ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) < ( ( 𝑁 + 1 ) − 1 ) )
77 76 olcd ⊢ ( 𝑁 ∈ ℕ → ( ( ( 𝑁 + 1 ) − 1 ) < 0 ∨ ( 𝑁 − 1 ) < ( ( 𝑁 + 1 ) − 1 ) ) )
78 bcval4 ⊢ ( ( ( 𝑁 − 1 ) ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) − 1 ) ∈ ℤ ∧ ( ( ( 𝑁 + 1 ) − 1 ) < 0 ∨ ( 𝑁 − 1 ) < ( ( 𝑁 + 1 ) − 1 ) ) ) → ( ( 𝑁 − 1 ) C ( ( 𝑁 + 1 ) − 1 ) ) = 0 )
79 13 72 77 78 syl3anc ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) C ( ( 𝑁 + 1 ) − 1 ) ) = 0 )
80 79 oveq2d ⊢ ( 𝑁 ∈ ℕ → ( ( - 1 ↑ ( ( 𝑁 + 1 ) − 1 ) ) · ( ( 𝑁 − 1 ) C ( ( 𝑁 + 1 ) − 1 ) ) ) = ( ( - 1 ↑ ( ( 𝑁 + 1 ) − 1 ) ) · 0 ) )
81 27 71 expcld ⊢ ( 𝑁 ∈ ℕ → ( - 1 ↑ ( ( 𝑁 + 1 ) − 1 ) ) ∈ ℂ )
82 81 mul01d ⊢ ( 𝑁 ∈ ℕ → ( ( - 1 ↑ ( ( 𝑁 + 1 ) − 1 ) ) · 0 ) = 0 )
83 80 82 eqtrd ⊢ ( 𝑁 ∈ ℕ → ( ( - 1 ↑ ( ( 𝑁 + 1 ) − 1 ) ) · ( ( 𝑁 − 1 ) C ( ( 𝑁 + 1 ) − 1 ) ) ) = 0 )
84 83 oveq2d ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( - 1 ↑ ( 𝑗 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑗 − 1 ) ) ) + ( ( - 1 ↑ ( ( 𝑁 + 1 ) − 1 ) ) · ( ( 𝑁 − 1 ) C ( ( 𝑁 + 1 ) − 1 ) ) ) ) = ( Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( - 1 ↑ ( 𝑗 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑗 − 1 ) ) ) + 0 ) )
85 oveq1 ⊢ ( 𝑗 = 𝑘 → ( 𝑗 − 1 ) = ( 𝑘 − 1 ) )
86 85 oveq2d ⊢ ( 𝑗 = 𝑘 → ( - 1 ↑ ( 𝑗 − 1 ) ) = ( - 1 ↑ ( 𝑘 − 1 ) ) )
87 85 oveq2d ⊢ ( 𝑗 = 𝑘 → ( ( 𝑁 − 1 ) C ( 𝑗 − 1 ) ) = ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) )
88 86 87 oveq12d ⊢ ( 𝑗 = 𝑘 → ( ( - 1 ↑ ( 𝑗 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑗 − 1 ) ) ) = ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) )
89 88 cbvsumv ⊢ Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( - 1 ↑ ( 𝑗 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑗 − 1 ) ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) )
90 89 a1i ⊢ ( 𝑁 ∈ ℕ → Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( - 1 ↑ ( 𝑗 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑗 − 1 ) ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) )
91 90 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( - 1 ↑ ( 𝑗 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑗 − 1 ) ) ) + 0 ) = ( Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) + 0 ) )
92 fzfid ⊢ ( 𝑁 ∈ ℕ → ( 1 ... 𝑁 ) ∈ Fin )
93 26 a1i ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → - 1 ∈ ℂ )
94 elfznn ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℕ )
95 nnm1nn0 ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 − 1 ) ∈ ℕ0 )
96 94 95 syl ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( 𝑘 − 1 ) ∈ ℕ0 )
97 96 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑘 − 1 ) ∈ ℕ0 )
98 93 97 expcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( - 1 ↑ ( 𝑘 − 1 ) ) ∈ ℂ )
99 elfzelz ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℤ )
100 elfzel1 ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 1 ∈ ℤ )
101 99 100 zsubcld ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( 𝑘 − 1 ) ∈ ℤ )
102 13 101 19 syl2an ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ∈ ℕ0 )
103 102 nn0cnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ∈ ℂ )
104 98 103 mulcld ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) ∈ ℂ )
105 92 104 fsumcl ⊢ ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) ∈ ℂ )
106 105 addridd ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) + 0 ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) )
107 91 106 eqtrd ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( - 1 ↑ ( 𝑗 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑗 − 1 ) ) ) + 0 ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) )
108 66 84 107 3eqtrd ⊢ ( 𝑁 ∈ ℕ → Σ 𝑗 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( ( - 1 ↑ ( 𝑗 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑗 − 1 ) ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) )
109 42 46 108 3eqtrd ⊢ ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 1 ) C 𝑘 ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) )
110 elnn0uz ⊢ ( 𝑁 ∈ ℕ0 ↔ 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
111 70 110 sylib ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
112 oveq2 ⊢ ( 𝑘 = 0 → ( - 1 ↑ 𝑘 ) = ( - 1 ↑ 0 ) )
113 oveq1 ⊢ ( 𝑘 = 0 → ( 𝑘 − 1 ) = ( 0 − 1 ) )
114 113 oveq2d ⊢ ( 𝑘 = 0 → ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) = ( ( 𝑁 − 1 ) C ( 0 − 1 ) ) )
115 112 114 oveq12d ⊢ ( 𝑘 = 0 → ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) = ( ( - 1 ↑ 0 ) · ( ( 𝑁 − 1 ) C ( 0 − 1 ) ) ) )
116 111 34 115 fsum1p ⊢ ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) = ( ( ( - 1 ↑ 0 ) · ( ( 𝑁 − 1 ) C ( 0 − 1 ) ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... 𝑁 ) ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) ) )
117 27 exp0d ⊢ ( 𝑁 ∈ ℕ → ( - 1 ↑ 0 ) = 1 )
118 0z ⊢ 0 ∈ ℤ
119 zsubcl ⊢ ( ( 0 ∈ ℤ ∧ 1 ∈ ℤ ) → ( 0 − 1 ) ∈ ℤ )
120 118 30 119 mp2an ⊢ ( 0 − 1 ) ∈ ℤ
121 120 a1i ⊢ ( 𝑁 ∈ ℕ → ( 0 − 1 ) ∈ ℤ )
122 0re ⊢ 0 ∈ ℝ
123 ltm1 ⊢ ( 0 ∈ ℝ → ( 0 − 1 ) < 0 )
124 122 123 mp1i ⊢ ( 𝑁 ∈ ℕ → ( 0 − 1 ) < 0 )
125 124 orcd ⊢ ( 𝑁 ∈ ℕ → ( ( 0 − 1 ) < 0 ∨ ( 𝑁 − 1 ) < ( 0 − 1 ) ) )
126 bcval4 ⊢ ( ( ( 𝑁 − 1 ) ∈ ℕ0 ∧ ( 0 − 1 ) ∈ ℤ ∧ ( ( 0 − 1 ) < 0 ∨ ( 𝑁 − 1 ) < ( 0 − 1 ) ) ) → ( ( 𝑁 − 1 ) C ( 0 − 1 ) ) = 0 )
127 13 121 125 126 syl3anc ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) C ( 0 − 1 ) ) = 0 )
128 117 127 oveq12d ⊢ ( 𝑁 ∈ ℕ → ( ( - 1 ↑ 0 ) · ( ( 𝑁 − 1 ) C ( 0 − 1 ) ) ) = ( 1 · 0 ) )
129 6 a1i ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℂ )
130 129 mul01d ⊢ ( 𝑁 ∈ ℕ → ( 1 · 0 ) = 0 )
131 128 130 eqtrd ⊢ ( 𝑁 ∈ ℕ → ( ( - 1 ↑ 0 ) · ( ( 𝑁 − 1 ) C ( 0 − 1 ) ) ) = 0 )
132 43 a1i ⊢ ( 𝑁 ∈ ℕ → ( 0 + 1 ) = 1 )
133 132 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( 0 + 1 ) ... 𝑁 ) = ( 1 ... 𝑁 ) )
134 99 zcnd ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℂ )
135 npcan1 ⊢ ( 𝑘 ∈ ℂ → ( ( 𝑘 − 1 ) + 1 ) = 𝑘 )
136 135 eqcomd ⊢ ( 𝑘 ∈ ℂ → 𝑘 = ( ( 𝑘 − 1 ) + 1 ) )
137 134 136 syl ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 = ( ( 𝑘 − 1 ) + 1 ) )
138 137 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 = ( ( 𝑘 − 1 ) + 1 ) )
139 138 oveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( - 1 ↑ 𝑘 ) = ( - 1 ↑ ( ( 𝑘 − 1 ) + 1 ) ) )
140 expp1 ⊢ ( ( - 1 ∈ ℂ ∧ ( 𝑘 − 1 ) ∈ ℕ0 ) → ( - 1 ↑ ( ( 𝑘 − 1 ) + 1 ) ) = ( ( - 1 ↑ ( 𝑘 − 1 ) ) · - 1 ) )
141 27 96 140 syl2an ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( - 1 ↑ ( ( 𝑘 − 1 ) + 1 ) ) = ( ( - 1 ↑ ( 𝑘 − 1 ) ) · - 1 ) )
142 139 141 eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( - 1 ↑ 𝑘 ) = ( ( - 1 ↑ ( 𝑘 − 1 ) ) · - 1 ) )
143 142 oveq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) = ( ( ( - 1 ↑ ( 𝑘 − 1 ) ) · - 1 ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) )
144 98 93 mulcomd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( - 1 ↑ ( 𝑘 − 1 ) ) · - 1 ) = ( - 1 · ( - 1 ↑ ( 𝑘 − 1 ) ) ) )
145 144 oveq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( ( - 1 ↑ ( 𝑘 − 1 ) ) · - 1 ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) = ( ( - 1 · ( - 1 ↑ ( 𝑘 − 1 ) ) ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) )
146 93 98 103 mulassd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( - 1 · ( - 1 ↑ ( 𝑘 − 1 ) ) ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) = ( - 1 · ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) ) )
147 143 145 146 3eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) = ( - 1 · ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) ) )
148 133 147 sumeq12rdv ⊢ ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( ( 0 + 1 ) ... 𝑁 ) ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( - 1 · ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) ) )
149 92 27 104 fsummulc2 ⊢ ( 𝑁 ∈ ℕ → ( - 1 · Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( - 1 · ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) ) )
150 148 149 eqtr4d ⊢ ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( ( 0 + 1 ) ... 𝑁 ) ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) = ( - 1 · Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) ) )
151 131 150 oveq12d ⊢ ( 𝑁 ∈ ℕ → ( ( ( - 1 ↑ 0 ) · ( ( 𝑁 − 1 ) C ( 0 − 1 ) ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... 𝑁 ) ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) ) = ( 0 + ( - 1 · Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) ) ) )
152 27 105 mulcld ⊢ ( 𝑁 ∈ ℕ → ( - 1 · Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) ) ∈ ℂ )
153 152 addlidd ⊢ ( 𝑁 ∈ ℕ → ( 0 + ( - 1 · Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) ) ) = ( - 1 · Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) ) )
154 116 151 153 3eqtrd ⊢ ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) = ( - 1 · Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) ) )
155 109 154 oveq12d ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑘 ∈ ( 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 ⊢ ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 1 ) C 𝑘 ) ) + ( ( - 1 ↑ 𝑘 ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) ) = ( Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) + ( - 1 · Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) ) ) )
157 105 mulm1d ⊢ ( 𝑁 ∈ ℕ → ( - 1 · Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) ) = - Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) )
158 157 oveq2d ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑘 ∈ ( 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 ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) + - Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) ) = 0 )
160 158 159 eqtrd ⊢ ( 𝑁 ∈ ℕ → ( Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) + ( - 1 · Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( - 1 ↑ ( 𝑘 − 1 ) ) · ( ( 𝑁 − 1 ) C ( 𝑘 − 1 ) ) ) ) ) = 0 )
161 24 156 160 3eqtrd ⊢ ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( - 1 ↑ 𝑘 ) · ( 𝑁 C 𝑘 ) ) = 0 )