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

Proof

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

Metamath Proof Explorer

Theorem altgsumbcALT

Proof