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	$⊢ N \in ℕ \to \sum_{k = 0}^{N} {(- 1)}^{k} (\binom{N}{k}) = 0$

Proof

Step	Hyp	Ref	Expression
1		1cnd	$⊢ N \in ℕ \to 1 \in ℂ$
2		negid	$⊢ 1 \in ℂ \to 1 + -1 = 0$
3	2	eqcomd	$⊢ 1 \in ℂ \to 0 = 1 + -1$
4	1 3	syl	$⊢ N \in ℕ \to 0 = 1 + -1$
5	4	oveq1d	$⊢ N \in ℕ \to 0^{N} = {(1 + -1)}^{N}$
6		0exp	$⊢ N \in ℕ \to 0^{N} = 0$
7	1	negcld	$⊢ N \in ℕ \to - 1 \in ℂ$
8		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
9		binom	$⊢ (1 \in ℂ \land - 1 \in ℂ \land N \in ℕ_{0}) \to {(1 + -1)}^{N} = \sum_{k = 0}^{N} (\binom{N}{k}) 1^{N - k} {(- 1)}^{k}$
10	1 7 8 9	syl3anc	$⊢ N \in ℕ \to {(1 + -1)}^{N} = \sum_{k = 0}^{N} (\binom{N}{k}) 1^{N - k} {(- 1)}^{k}$
11		nnz	$⊢ N \in ℕ \to N \in ℤ$
12		elfzelz	$⊢ k \in (0 \dots N) \to k \in ℤ$
13		zsubcl	$⊢ (N \in ℤ \land k \in ℤ) \to N - k \in ℤ$
14	11 12 13	syl2an	$⊢ (N \in ℕ \land k \in (0 \dots N)) \to N - k \in ℤ$
15		1exp	$⊢ N - k \in ℤ \to 1^{N - k} = 1$
16	14 15	syl	$⊢ (N \in ℕ \land k \in (0 \dots N)) \to 1^{N - k} = 1$
17	16	oveq1d	$⊢ (N \in ℕ \land k \in (0 \dots N)) \to 1^{N - k} {(- 1)}^{k} = 1 {(- 1)}^{k}$
18		neg1cn	$⊢ - 1 \in ℂ$
19	18	a1i	$⊢ N \in ℕ \to - 1 \in ℂ$
20		elfznn0	$⊢ k \in (0 \dots N) \to k \in ℕ_{0}$
21		expcl	$⊢ (- 1 \in ℂ \land k \in ℕ_{0}) \to {(- 1)}^{k} \in ℂ$
22	19 20 21	syl2an	$⊢ (N \in ℕ \land k \in (0 \dots N)) \to {(- 1)}^{k} \in ℂ$
23	22	mullidd	$⊢ (N \in ℕ \land k \in (0 \dots N)) \to 1 {(- 1)}^{k} = {(- 1)}^{k}$
24	17 23	eqtrd	$⊢ (N \in ℕ \land k \in (0 \dots N)) \to 1^{N - k} {(- 1)}^{k} = {(- 1)}^{k}$
25	24	oveq2d	$⊢ (N \in ℕ \land k \in (0 \dots N)) \to (\binom{N}{k}) 1^{N - k} {(- 1)}^{k} = (\binom{N}{k}) {(- 1)}^{k}$
26		bccl	$⊢ (N \in ℕ_{0} \land k \in ℤ) \to (\binom{N}{k}) \in ℕ_{0}$
27	8 12 26	syl2an	$⊢ (N \in ℕ \land k \in (0 \dots N)) \to (\binom{N}{k}) \in ℕ_{0}$
28	27	nn0cnd	$⊢ (N \in ℕ \land k \in (0 \dots N)) \to (\binom{N}{k}) \in ℂ$
29	28 22	mulcomd	$⊢ (N \in ℕ \land k \in (0 \dots N)) \to (\binom{N}{k}) {(- 1)}^{k} = {(- 1)}^{k} (\binom{N}{k})$
30	25 29	eqtrd	$⊢ (N \in ℕ \land k \in (0 \dots N)) \to (\binom{N}{k}) 1^{N - k} {(- 1)}^{k} = {(- 1)}^{k} (\binom{N}{k})$
31	30	sumeq2dv	$⊢ N \in ℕ \to \sum_{k = 0}^{N} (\binom{N}{k}) 1^{N - k} {(- 1)}^{k} = \sum_{k = 0}^{N} {(- 1)}^{k} (\binom{N}{k})$
32	10 31	eqtrd	$⊢ N \in ℕ \to {(1 + -1)}^{N} = \sum_{k = 0}^{N} {(- 1)}^{k} (\binom{N}{k})$
33	5 6 32	3eqtr3rd	$⊢ N \in ℕ \to \sum_{k = 0}^{N} {(- 1)}^{k} (\binom{N}{k}) = 0$

Metamath Proof Explorer

Theorem altgsumbc

Proof