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 )