Metamath Proof Explorer

Theorem altgsumbc

Description: The sum of binomial coefficients for a fixed positive N with alternating signs is zero. Notice that this is not valid for N = 0 (since ( ( -u 1 ^ 0 ) x. ( 0 _C 0 ) ) = ( 1 x. 1 ) = 1 ). For a proof using Pascal's rule ( bcpascm1 ) instead of the binomial theorem ( binom ), see altgsumbcALT . (Contributed by AV, 13-Sep-2019)

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

Proof

Step Hyp Ref Expression
1 1cnd ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℂ )
2 negid ⊢ ( 1 ∈ ℂ → ( 1 + - 1 ) = 0 )
3 2 eqcomd ⊢ ( 1 ∈ ℂ → 0 = ( 1 + - 1 ) )
4 1 3 syl ⊢ ( 𝑁 ∈ ℕ → 0 = ( 1 + - 1 ) )
5 4 oveq1d ⊢ ( 𝑁 ∈ ℕ → ( 0 ↑ 𝑁 ) = ( ( 1 + - 1 ) ↑ 𝑁 ) )
6 0exp ⊢ ( 𝑁 ∈ ℕ → ( 0 ↑ 𝑁 ) = 0 )
7 1 negcld ⊢ ( 𝑁 ∈ ℕ → - 1 ∈ ℂ )
8 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
9 binom ⊢ ( ( 1 ∈ ℂ ∧ - 1 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( 1 + - 1 ) ↑ 𝑁 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 1 ↑ ( 𝑁 − 𝑘 ) ) · ( - 1 ↑ 𝑘 ) ) ) )
10 1 7 8 9 syl3anc ⊢ ( 𝑁 ∈ ℕ → ( ( 1 + - 1 ) ↑ 𝑁 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 1 ↑ ( 𝑁 − 𝑘 ) ) · ( - 1 ↑ 𝑘 ) ) ) )
11 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
12 elfzelz ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℤ )
13 zsubcl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑁 − 𝑘 ) ∈ ℤ )
14 11 12 13 syl2an ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 − 𝑘 ) ∈ ℤ )
15 1exp ⊢ ( ( 𝑁 − 𝑘 ) ∈ ℤ → ( 1 ↑ ( 𝑁 − 𝑘 ) ) = 1 )
16 14 15 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 1 ↑ ( 𝑁 − 𝑘 ) ) = 1 )
17 16 oveq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 1 ↑ ( 𝑁 − 𝑘 ) ) · ( - 1 ↑ 𝑘 ) ) = ( 1 · ( - 1 ↑ 𝑘 ) ) )
18 neg1cn ⊢ - 1 ∈ ℂ
19 18 a1i ⊢ ( 𝑁 ∈ ℕ → - 1 ∈ ℂ )
20 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
21 expcl ⊢ ( ( - 1 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( - 1 ↑ 𝑘 ) ∈ ℂ )
22 19 20 21 syl2an ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( - 1 ↑ 𝑘 ) ∈ ℂ )
23 22 mullidd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 1 · ( - 1 ↑ 𝑘 ) ) = ( - 1 ↑ 𝑘 ) )
24 17 23 eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 1 ↑ ( 𝑁 − 𝑘 ) ) · ( - 1 ↑ 𝑘 ) ) = ( - 1 ↑ 𝑘 ) )
25 24 oveq2d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 C 𝑘 ) · ( ( 1 ↑ ( 𝑁 − 𝑘 ) ) · ( - 1 ↑ 𝑘 ) ) ) = ( ( 𝑁 C 𝑘 ) · ( - 1 ↑ 𝑘 ) ) )
26 bccl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℤ ) → ( 𝑁 C 𝑘 ) ∈ ℕ0 )
27 8 12 26 syl2an ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝑘 ) ∈ ℕ0 )
28 27 nn0cnd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝑘 ) ∈ ℂ )
29 28 22 mulcomd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 C 𝑘 ) · ( - 1 ↑ 𝑘 ) ) = ( ( - 1 ↑ 𝑘 ) · ( 𝑁 C 𝑘 ) ) )
30 25 29 eqtrd ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 C 𝑘 ) · ( ( 1 ↑ ( 𝑁 − 𝑘 ) ) · ( - 1 ↑ 𝑘 ) ) ) = ( ( - 1 ↑ 𝑘 ) · ( 𝑁 C 𝑘 ) ) )
31 30 sumeq2dv ⊢ ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 1 ↑ ( 𝑁 − 𝑘 ) ) · ( - 1 ↑ 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( - 1 ↑ 𝑘 ) · ( 𝑁 C 𝑘 ) ) )
32 10 31 eqtrd ⊢ ( 𝑁 ∈ ℕ → ( ( 1 + - 1 ) ↑ 𝑁 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( - 1 ↑ 𝑘 ) · ( 𝑁 C 𝑘 ) ) )
33 5 6 32 3eqtr3rd ⊢ ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( - 1 ↑ 𝑘 ) · ( 𝑁 C 𝑘 ) ) = 0 )