bccolsum

Description: A column-sum rule for binomial coefficients. (Contributed by Scott Fenton, 24-Jun-2020)

		Ref	Expression
	Assertion	bccolsum	$⊢ (N \in ℕ_{0} \land C \in ℕ_{0}) \to \sum_{k = 0}^{N} (\binom{k}{C}) = (\binom{N + 1}{C + 1})$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ m = 0 \to (0 \dots m) = (0 \dots 0)$
2	1	sumeq1d	$⊢ m = 0 \to \sum_{k = 0}^{m} (\binom{k}{C}) = \sum_{k = 0}^{0} (\binom{k}{C})$
3		oveq1	$⊢ m = 0 \to m + 1 = 0 + 1$
4		0p1e1	$⊢ 0 + 1 = 1$
5	3 4	eqtrdi	$⊢ m = 0 \to m + 1 = 1$
6	5	oveq1d	$⊢ m = 0 \to (\binom{m + 1}{C + 1}) = (\binom{1}{C + 1})$
7	2 6	eqeq12d	$⊢ m = 0 \to (\sum_{k = 0}^{m} (\binom{k}{C}) = (\binom{m + 1}{C + 1}) \leftrightarrow \sum_{k = 0}^{0} (\binom{k}{C}) = (\binom{1}{C + 1}))$
8	7	imbi2d	$⊢ m = 0 \to ((C \in ℕ_{0} \to \sum_{k = 0}^{m} (\binom{k}{C}) = (\binom{m + 1}{C + 1})) \leftrightarrow (C \in ℕ_{0} \to \sum_{k = 0}^{0} (\binom{k}{C}) = (\binom{1}{C + 1})))$
9		oveq2	$⊢ m = n \to (0 \dots m) = (0 \dots n)$
10	9	sumeq1d	$⊢ m = n \to \sum_{k = 0}^{m} (\binom{k}{C}) = \sum_{k = 0}^{n} (\binom{k}{C})$
11		oveq1	$⊢ m = n \to m + 1 = n + 1$
12	11	oveq1d	$⊢ m = n \to (\binom{m + 1}{C + 1}) = (\binom{n + 1}{C + 1})$
13	10 12	eqeq12d	$⊢ m = n \to (\sum_{k = 0}^{m} (\binom{k}{C}) = (\binom{m + 1}{C + 1}) \leftrightarrow \sum_{k = 0}^{n} (\binom{k}{C}) = (\binom{n + 1}{C + 1}))$
14	13	imbi2d	$⊢ m = n \to ((C \in ℕ_{0} \to \sum_{k = 0}^{m} (\binom{k}{C}) = (\binom{m + 1}{C + 1})) \leftrightarrow (C \in ℕ_{0} \to \sum_{k = 0}^{n} (\binom{k}{C}) = (\binom{n + 1}{C + 1})))$
15		oveq2	$⊢ m = n + 1 \to (0 \dots m) = (0 \dots n + 1)$
16	15	sumeq1d	$⊢ m = n + 1 \to \sum_{k = 0}^{m} (\binom{k}{C}) = \sum_{k = 0}^{n + 1} (\binom{k}{C})$
17		oveq1	$⊢ m = n + 1 \to m + 1 = n + 1 + 1$
18	17	oveq1d	$⊢ m = n + 1 \to (\binom{m + 1}{C + 1}) = (\binom{n + 1 + 1}{C + 1})$
19	16 18	eqeq12d	$⊢ m = n + 1 \to (\sum_{k = 0}^{m} (\binom{k}{C}) = (\binom{m + 1}{C + 1}) \leftrightarrow \sum_{k = 0}^{n + 1} (\binom{k}{C}) = (\binom{n + 1 + 1}{C + 1}))$
20	19	imbi2d	$⊢ m = n + 1 \to ((C \in ℕ_{0} \to \sum_{k = 0}^{m} (\binom{k}{C}) = (\binom{m + 1}{C + 1})) \leftrightarrow (C \in ℕ_{0} \to \sum_{k = 0}^{n + 1} (\binom{k}{C}) = (\binom{n + 1 + 1}{C + 1})))$
21		oveq2	$⊢ m = N \to (0 \dots m) = (0 \dots N)$
22	21	sumeq1d	$⊢ m = N \to \sum_{k = 0}^{m} (\binom{k}{C}) = \sum_{k = 0}^{N} (\binom{k}{C})$
23		oveq1	$⊢ m = N \to m + 1 = N + 1$
24	23	oveq1d	$⊢ m = N \to (\binom{m + 1}{C + 1}) = (\binom{N + 1}{C + 1})$
25	22 24	eqeq12d	$⊢ m = N \to (\sum_{k = 0}^{m} (\binom{k}{C}) = (\binom{m + 1}{C + 1}) \leftrightarrow \sum_{k = 0}^{N} (\binom{k}{C}) = (\binom{N + 1}{C + 1}))$
26	25	imbi2d	$⊢ m = N \to ((C \in ℕ_{0} \to \sum_{k = 0}^{m} (\binom{k}{C}) = (\binom{m + 1}{C + 1})) \leftrightarrow (C \in ℕ_{0} \to \sum_{k = 0}^{N} (\binom{k}{C}) = (\binom{N + 1}{C + 1})))$
27		0z	$⊢ 0 \in ℤ$
28		0nn0	$⊢ 0 \in ℕ_{0}$
29		nn0z	$⊢ C \in ℕ_{0} \to C \in ℤ$
30		bccl	$⊢ (0 \in ℕ_{0} \land C \in ℤ) \to (\binom{0}{C}) \in ℕ_{0}$
31	28 29 30	sylancr	$⊢ C \in ℕ_{0} \to (\binom{0}{C}) \in ℕ_{0}$
32	31	nn0cnd	$⊢ C \in ℕ_{0} \to (\binom{0}{C}) \in ℂ$
33		oveq1	$⊢ k = 0 \to (\binom{k}{C}) = (\binom{0}{C})$
34	33	fsum1	$⊢ (0 \in ℤ \land (\binom{0}{C}) \in ℂ) \to \sum_{k = 0}^{0} (\binom{k}{C}) = (\binom{0}{C})$
35	27 32 34	sylancr	$⊢ C \in ℕ_{0} \to \sum_{k = 0}^{0} (\binom{k}{C}) = (\binom{0}{C})$
36		elnn0	$⊢ C \in ℕ_{0} \leftrightarrow (C \in ℕ \lor C = 0)$
37		1red	$⊢ C \in ℕ \to 1 \in ℝ$
38		nnrp	$⊢ C \in ℕ \to C \in ℝ^{+}$
39	37 38	ltaddrp2d	$⊢ C \in ℕ \to 1 < C + 1$
40		peano2nn	$⊢ C \in ℕ \to C + 1 \in ℕ$
41	40	nnred	$⊢ C \in ℕ \to C + 1 \in ℝ$
42	37 41	ltnled	$⊢ C \in ℕ \to (1 < C + 1 \leftrightarrow \neg C + 1 \leq 1)$
43	39 42	mpbid	$⊢ C \in ℕ \to \neg C + 1 \leq 1$
44		elfzle2	$⊢ C + 1 \in (0 \dots 1) \to C + 1 \leq 1$
45	43 44	nsyl	$⊢ C \in ℕ \to \neg C + 1 \in (0 \dots 1)$
46	45	iffalsed	$⊢ C \in ℕ \to if (C + 1 \in (0 \dots 1), \frac{1!}{(1 - (C + 1))! (C + 1)!}, 0) = 0$
47		1nn0	$⊢ 1 \in ℕ_{0}$
48	40	nnzd	$⊢ C \in ℕ \to C + 1 \in ℤ$
49		bcval	$⊢ (1 \in ℕ_{0} \land C + 1 \in ℤ) \to (\binom{1}{C + 1}) = if (C + 1 \in (0 \dots 1), \frac{1!}{(1 - (C + 1))! (C + 1)!}, 0)$
50	47 48 49	sylancr	$⊢ C \in ℕ \to (\binom{1}{C + 1}) = if (C + 1 \in (0 \dots 1), \frac{1!}{(1 - (C + 1))! (C + 1)!}, 0)$
51		bc0k	$⊢ C \in ℕ \to (\binom{0}{C}) = 0$
52	46 50 51	3eqtr4rd	$⊢ C \in ℕ \to (\binom{0}{C}) = (\binom{1}{C + 1})$
53		bcnn	$⊢ 0 \in ℕ_{0} \to (\binom{0}{0}) = 1$
54	28 53	ax-mp	$⊢ (\binom{0}{0}) = 1$
55		bcnn	$⊢ 1 \in ℕ_{0} \to (\binom{1}{1}) = 1$
56	47 55	ax-mp	$⊢ (\binom{1}{1}) = 1$
57	54 56	eqtr4i	$⊢ (\binom{0}{0}) = (\binom{1}{1})$
58		oveq2	$⊢ C = 0 \to (\binom{0}{C}) = (\binom{0}{0})$
59		oveq1	$⊢ C = 0 \to C + 1 = 0 + 1$
60	59 4	eqtrdi	$⊢ C = 0 \to C + 1 = 1$
61	60	oveq2d	$⊢ C = 0 \to (\binom{1}{C + 1}) = (\binom{1}{1})$
62	57 58 61	3eqtr4a	$⊢ C = 0 \to (\binom{0}{C}) = (\binom{1}{C + 1})$
63	52 62	jaoi	$⊢ (C \in ℕ \lor C = 0) \to (\binom{0}{C}) = (\binom{1}{C + 1})$
64	36 63	sylbi	$⊢ C \in ℕ_{0} \to (\binom{0}{C}) = (\binom{1}{C + 1})$
65	35 64	eqtrd	$⊢ C \in ℕ_{0} \to \sum_{k = 0}^{0} (\binom{k}{C}) = (\binom{1}{C + 1})$
66		elnn0uz	$⊢ n \in ℕ_{0} \leftrightarrow n \in ℤ_{\geq 0}$
67	66	biimpi	$⊢ n \in ℕ_{0} \to n \in ℤ_{\geq 0}$
68	67	adantr	$⊢ (n \in ℕ_{0} \land C \in ℕ_{0}) \to n \in ℤ_{\geq 0}$
69		elfznn0	$⊢ k \in (0 \dots n + 1) \to k \in ℕ_{0}$
70	69	adantl	$⊢ ((n \in ℕ_{0} \land C \in ℕ_{0}) \land k \in (0 \dots n + 1)) \to k \in ℕ_{0}$
71		simplr	$⊢ ((n \in ℕ_{0} \land C \in ℕ_{0}) \land k \in (0 \dots n + 1)) \to C \in ℕ_{0}$
72	71	nn0zd	$⊢ ((n \in ℕ_{0} \land C \in ℕ_{0}) \land k \in (0 \dots n + 1)) \to C \in ℤ$
73		bccl	$⊢ (k \in ℕ_{0} \land C \in ℤ) \to (\binom{k}{C}) \in ℕ_{0}$
74	70 72 73	syl2anc	$⊢ ((n \in ℕ_{0} \land C \in ℕ_{0}) \land k \in (0 \dots n + 1)) \to (\binom{k}{C}) \in ℕ_{0}$
75	74	nn0cnd	$⊢ ((n \in ℕ_{0} \land C \in ℕ_{0}) \land k \in (0 \dots n + 1)) \to (\binom{k}{C}) \in ℂ$
76		oveq1	$⊢ k = n + 1 \to (\binom{k}{C}) = (\binom{n + 1}{C})$
77	68 75 76	fsump1	$⊢ (n \in ℕ_{0} \land C \in ℕ_{0}) \to \sum_{k = 0}^{n + 1} (\binom{k}{C}) = \sum_{k = 0}^{n} (\binom{k}{C}) + (\binom{n + 1}{C})$
78	77	adantr	$⊢ ((n \in ℕ_{0} \land C \in ℕ_{0}) \land \sum_{k = 0}^{n} (\binom{k}{C}) = (\binom{n + 1}{C + 1})) \to \sum_{k = 0}^{n + 1} (\binom{k}{C}) = \sum_{k = 0}^{n} (\binom{k}{C}) + (\binom{n + 1}{C})$
79		id	$⊢ \sum_{k = 0}^{n} (\binom{k}{C}) = (\binom{n + 1}{C + 1}) \to \sum_{k = 0}^{n} (\binom{k}{C}) = (\binom{n + 1}{C + 1})$
80		nn0cn	$⊢ C \in ℕ_{0} \to C \in ℂ$
81	80	adantl	$⊢ (n \in ℕ_{0} \land C \in ℕ_{0}) \to C \in ℂ$
82		1cnd	$⊢ (n \in ℕ_{0} \land C \in ℕ_{0}) \to 1 \in ℂ$
83	81 82	pncand	$⊢ (n \in ℕ_{0} \land C \in ℕ_{0}) \to C + 1 - 1 = C$
84	83	oveq2d	$⊢ (n \in ℕ_{0} \land C \in ℕ_{0}) \to (\binom{n + 1}{C + 1 - 1}) = (\binom{n + 1}{C})$
85	84	eqcomd	$⊢ (n \in ℕ_{0} \land C \in ℕ_{0}) \to (\binom{n + 1}{C}) = (\binom{n + 1}{C + 1 - 1})$
86	79 85	oveqan12rd	$⊢ ((n \in ℕ_{0} \land C \in ℕ_{0}) \land \sum_{k = 0}^{n} (\binom{k}{C}) = (\binom{n + 1}{C + 1})) \to \sum_{k = 0}^{n} (\binom{k}{C}) + (\binom{n + 1}{C}) = (\binom{n + 1}{C + 1}) + (\binom{n + 1}{C + 1 - 1})$
87		peano2nn0	$⊢ n \in ℕ_{0} \to n + 1 \in ℕ_{0}$
88		peano2nn0	$⊢ C \in ℕ_{0} \to C + 1 \in ℕ_{0}$
89	88	nn0zd	$⊢ C \in ℕ_{0} \to C + 1 \in ℤ$
90		bcpasc	$⊢ (n + 1 \in ℕ_{0} \land C + 1 \in ℤ) \to (\binom{n + 1}{C + 1}) + (\binom{n + 1}{C + 1 - 1}) = (\binom{n + 1 + 1}{C + 1})$
91	87 89 90	syl2an	$⊢ (n \in ℕ_{0} \land C \in ℕ_{0}) \to (\binom{n + 1}{C + 1}) + (\binom{n + 1}{C + 1 - 1}) = (\binom{n + 1 + 1}{C + 1})$
92	91	adantr	$⊢ ((n \in ℕ_{0} \land C \in ℕ_{0}) \land \sum_{k = 0}^{n} (\binom{k}{C}) = (\binom{n + 1}{C + 1})) \to (\binom{n + 1}{C + 1}) + (\binom{n + 1}{C + 1 - 1}) = (\binom{n + 1 + 1}{C + 1})$
93	78 86 92	3eqtrd	$⊢ ((n \in ℕ_{0} \land C \in ℕ_{0}) \land \sum_{k = 0}^{n} (\binom{k}{C}) = (\binom{n + 1}{C + 1})) \to \sum_{k = 0}^{n + 1} (\binom{k}{C}) = (\binom{n + 1 + 1}{C + 1})$
94	93	exp31	$⊢ n \in ℕ_{0} \to (C \in ℕ_{0} \to (\sum_{k = 0}^{n} (\binom{k}{C}) = (\binom{n + 1}{C + 1}) \to \sum_{k = 0}^{n + 1} (\binom{k}{C}) = (\binom{n + 1 + 1}{C + 1})))$
95	94	a2d	$⊢ n \in ℕ_{0} \to ((C \in ℕ_{0} \to \sum_{k = 0}^{n} (\binom{k}{C}) = (\binom{n + 1}{C + 1})) \to (C \in ℕ_{0} \to \sum_{k = 0}^{n + 1} (\binom{k}{C}) = (\binom{n + 1 + 1}{C + 1})))$
96	8 14 20 26 65 95	nn0ind	$⊢ N \in ℕ_{0} \to (C \in ℕ_{0} \to \sum_{k = 0}^{N} (\binom{k}{C}) = (\binom{N + 1}{C + 1}))$
97	96	imp	$⊢ (N \in ℕ_{0} \land C \in ℕ_{0}) \to \sum_{k = 0}^{N} (\binom{k}{C}) = (\binom{N + 1}{C + 1})$

Metamath Proof Explorer

Theorem bccolsum

Proof