bcxmas

Description: Parallel summation (Christmas Stocking) theorem for Pascal's Triangle. (Contributed by Paul Chapman, 18-May-2007) (Revised by Mario Carneiro, 24-Apr-2014)

		Ref	Expression
	Assertion	bcxmas	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0}) \to (\binom{N + 1 + M}{M}) = \sum_{j = 0}^{M} (\binom{N + j}{j})$

Proof

Step	Hyp	Ref	Expression
1		bcxmaslem1	$⊢ m = 0 \to (\binom{N + 1 + m}{m}) = (\binom{N + 1 + 0}{0})$
2		oveq2	$⊢ m = 0 \to (0 \dots m) = (0 \dots 0)$
3	2	sumeq1d	$⊢ m = 0 \to \sum_{j = 0}^{m} (\binom{N + j}{j}) = \sum_{j = 0}^{0} (\binom{N + j}{j})$
4	1 3	eqeq12d	$⊢ m = 0 \to ((\binom{N + 1 + m}{m}) = \sum_{j = 0}^{m} (\binom{N + j}{j}) \leftrightarrow (\binom{N + 1 + 0}{0}) = \sum_{j = 0}^{0} (\binom{N + j}{j}))$
5		bcxmaslem1	$⊢ m = k \to (\binom{N + 1 + m}{m}) = (\binom{N + 1 + k}{k})$
6		oveq2	$⊢ m = k \to (0 \dots m) = (0 \dots k)$
7	6	sumeq1d	$⊢ m = k \to \sum_{j = 0}^{m} (\binom{N + j}{j}) = \sum_{j = 0}^{k} (\binom{N + j}{j})$
8	5 7	eqeq12d	$⊢ m = k \to ((\binom{N + 1 + m}{m}) = \sum_{j = 0}^{m} (\binom{N + j}{j}) \leftrightarrow (\binom{N + 1 + k}{k}) = \sum_{j = 0}^{k} (\binom{N + j}{j}))$
9		bcxmaslem1	$⊢ m = k + 1 \to (\binom{N + 1 + m}{m}) = (\binom{N + 1 + k + 1}{k + 1})$
10		oveq2	$⊢ m = k + 1 \to (0 \dots m) = (0 \dots k + 1)$
11	10	sumeq1d	$⊢ m = k + 1 \to \sum_{j = 0}^{m} (\binom{N + j}{j}) = \sum_{j = 0}^{k + 1} (\binom{N + j}{j})$
12	9 11	eqeq12d	$⊢ m = k + 1 \to ((\binom{N + 1 + m}{m}) = \sum_{j = 0}^{m} (\binom{N + j}{j}) \leftrightarrow (\binom{N + 1 + k + 1}{k + 1}) = \sum_{j = 0}^{k + 1} (\binom{N + j}{j}))$
13		bcxmaslem1	$⊢ m = M \to (\binom{N + 1 + m}{m}) = (\binom{N + 1 + M}{M})$
14		oveq2	$⊢ m = M \to (0 \dots m) = (0 \dots M)$
15	14	sumeq1d	$⊢ m = M \to \sum_{j = 0}^{m} (\binom{N + j}{j}) = \sum_{j = 0}^{M} (\binom{N + j}{j})$
16	13 15	eqeq12d	$⊢ m = M \to ((\binom{N + 1 + m}{m}) = \sum_{j = 0}^{m} (\binom{N + j}{j}) \leftrightarrow (\binom{N + 1 + M}{M}) = \sum_{j = 0}^{M} (\binom{N + j}{j}))$
17		0nn0	$⊢ 0 \in ℕ_{0}$
18		nn0addcl	$⊢ (N \in ℕ_{0} \land 0 \in ℕ_{0}) \to N + 0 \in ℕ_{0}$
19		bcn0	$⊢ N + 0 \in ℕ_{0} \to (\binom{N + 0}{0}) = 1$
20	18 19	syl	$⊢ (N \in ℕ_{0} \land 0 \in ℕ_{0}) \to (\binom{N + 0}{0}) = 1$
21	17 20	mpan2	$⊢ N \in ℕ_{0} \to (\binom{N + 0}{0}) = 1$
22		0z	$⊢ 0 \in ℤ$
23		1nn0	$⊢ 1 \in ℕ_{0}$
24	21 23	eqeltrdi	$⊢ N \in ℕ_{0} \to (\binom{N + 0}{0}) \in ℕ_{0}$
25	24	nn0cnd	$⊢ N \in ℕ_{0} \to (\binom{N + 0}{0}) \in ℂ$
26		bcxmaslem1	$⊢ j = 0 \to (\binom{N + j}{j}) = (\binom{N + 0}{0})$
27	26	fsum1	$⊢ (0 \in ℤ \land (\binom{N + 0}{0}) \in ℂ) \to \sum_{j = 0}^{0} (\binom{N + j}{j}) = (\binom{N + 0}{0})$
28	22 25 27	sylancr	$⊢ N \in ℕ_{0} \to \sum_{j = 0}^{0} (\binom{N + j}{j}) = (\binom{N + 0}{0})$
29		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
30		nn0addcl	$⊢ (N + 1 \in ℕ_{0} \land 0 \in ℕ_{0}) \to N + 1 + 0 \in ℕ_{0}$
31	29 17 30	sylancl	$⊢ N \in ℕ_{0} \to N + 1 + 0 \in ℕ_{0}$
32		bcn0	$⊢ N + 1 + 0 \in ℕ_{0} \to (\binom{N + 1 + 0}{0}) = 1$
33	31 32	syl	$⊢ N \in ℕ_{0} \to (\binom{N + 1 + 0}{0}) = 1$
34	21 28 33	3eqtr4rd	$⊢ N \in ℕ_{0} \to (\binom{N + 1 + 0}{0}) = \sum_{j = 0}^{0} (\binom{N + j}{j})$
35		elnn0uz	$⊢ k \in ℕ_{0} \leftrightarrow k \in ℤ_{\geq 0}$
36	35	bilani	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to k \in ℤ_{\geq 0}$
37		simpl	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to N \in ℕ_{0}$
38		elfznn0	$⊢ j \in (0 \dots k + 1) \to j \in ℕ_{0}$
39		nn0addcl	$⊢ (N \in ℕ_{0} \land j \in ℕ_{0}) \to N + j \in ℕ_{0}$
40	37 38 39	syl2an	$⊢ ((N \in ℕ_{0} \land k \in ℕ_{0}) \land j \in (0 \dots k + 1)) \to N + j \in ℕ_{0}$
41		elfzelz	$⊢ j \in (0 \dots k + 1) \to j \in ℤ$
42	41	adantl	$⊢ ((N \in ℕ_{0} \land k \in ℕ_{0}) \land j \in (0 \dots k + 1)) \to j \in ℤ$
43		bccl	$⊢ (N + j \in ℕ_{0} \land j \in ℤ) \to (\binom{N + j}{j}) \in ℕ_{0}$
44	40 42 43	syl2anc	$⊢ ((N \in ℕ_{0} \land k \in ℕ_{0}) \land j \in (0 \dots k + 1)) \to (\binom{N + j}{j}) \in ℕ_{0}$
45	44	nn0cnd	$⊢ ((N \in ℕ_{0} \land k \in ℕ_{0}) \land j \in (0 \dots k + 1)) \to (\binom{N + j}{j}) \in ℂ$
46		bcxmaslem1	$⊢ j = k + 1 \to (\binom{N + j}{j}) = (\binom{N + k + 1}{k + 1})$
47	36 45 46	fsump1	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to \sum_{j = 0}^{k + 1} (\binom{N + j}{j}) = \sum_{j = 0}^{k} (\binom{N + j}{j}) + (\binom{N + k + 1}{k + 1})$
48		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
49	48	adantr	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to N \in ℂ$
50		nn0cn	$⊢ k \in ℕ_{0} \to k \in ℂ$
51	50	adantl	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to k \in ℂ$
52		1cnd	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to 1 \in ℂ$
53		add32r	$⊢ (N \in ℂ \land k \in ℂ \land 1 \in ℂ) \to N + k + 1 = N + 1 + k$
54	49 51 52 53	syl3anc	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to N + k + 1 = N + 1 + k$
55	54	oveq1d	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to (\binom{N + k + 1}{k + 1}) = (\binom{N + 1 + k}{k + 1})$
56	55	oveq2d	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to \sum_{j = 0}^{k} (\binom{N + j}{j}) + (\binom{N + k + 1}{k + 1}) = \sum_{j = 0}^{k} (\binom{N + j}{j}) + (\binom{N + 1 + k}{k + 1})$
57	47 56	eqtrd	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to \sum_{j = 0}^{k + 1} (\binom{N + j}{j}) = \sum_{j = 0}^{k} (\binom{N + j}{j}) + (\binom{N + 1 + k}{k + 1})$
58	57	adantr	$⊢ ((N \in ℕ_{0} \land k \in ℕ_{0}) \land (\binom{N + 1 + k}{k}) = \sum_{j = 0}^{k} (\binom{N + j}{j})) \to \sum_{j = 0}^{k + 1} (\binom{N + j}{j}) = \sum_{j = 0}^{k} (\binom{N + j}{j}) + (\binom{N + 1 + k}{k + 1})$
59		oveq1	$⊢ (\binom{N + 1 + k}{k}) = \sum_{j = 0}^{k} (\binom{N + j}{j}) \to (\binom{N + 1 + k}{k}) + (\binom{N + 1 + k}{k + 1}) = \sum_{j = 0}^{k} (\binom{N + j}{j}) + (\binom{N + 1 + k}{k + 1})$
60	59	adantl	$⊢ ((N \in ℕ_{0} \land k \in ℕ_{0}) \land (\binom{N + 1 + k}{k}) = \sum_{j = 0}^{k} (\binom{N + j}{j})) \to (\binom{N + 1 + k}{k}) + (\binom{N + 1 + k}{k + 1}) = \sum_{j = 0}^{k} (\binom{N + j}{j}) + (\binom{N + 1 + k}{k + 1})$
61		ax-1cn	$⊢ 1 \in ℂ$
62		pncan	$⊢ (k \in ℂ \land 1 \in ℂ) \to k + 1 - 1 = k$
63	51 61 62	sylancl	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to k + 1 - 1 = k$
64	63	oveq2d	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to (\binom{N + 1 + k}{k + 1 - 1}) = (\binom{N + 1 + k}{k})$
65	64	oveq2d	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to (\binom{N + 1 + k}{k + 1}) + (\binom{N + 1 + k}{k + 1 - 1}) = (\binom{N + 1 + k}{k + 1}) + (\binom{N + 1 + k}{k})$
66		nn0addcl	$⊢ (N + 1 \in ℕ_{0} \land k \in ℕ_{0}) \to N + 1 + k \in ℕ_{0}$
67	29 66	sylan	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to N + 1 + k \in ℕ_{0}$
68		nn0p1nn	$⊢ k \in ℕ_{0} \to k + 1 \in ℕ$
69	68	adantl	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to k + 1 \in ℕ$
70	69	nnzd	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to k + 1 \in ℤ$
71		bcpasc	$⊢ (N + 1 + k \in ℕ_{0} \land k + 1 \in ℤ) \to (\binom{N + 1 + k}{k + 1}) + (\binom{N + 1 + k}{k + 1 - 1}) = (\binom{(N + 1) + k + 1}{k + 1})$
72	67 70 71	syl2anc	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to (\binom{N + 1 + k}{k + 1}) + (\binom{N + 1 + k}{k + 1 - 1}) = (\binom{(N + 1) + k + 1}{k + 1})$
73	65 72	eqtr3d	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to (\binom{N + 1 + k}{k + 1}) + (\binom{N + 1 + k}{k}) = (\binom{(N + 1) + k + 1}{k + 1})$
74		nn0p1nn	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ$
75		nnnn0addcl	$⊢ (N + 1 \in ℕ \land k \in ℕ_{0}) \to N + 1 + k \in ℕ$
76	74 75	sylan	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to N + 1 + k \in ℕ$
77	76	nnnn0d	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to N + 1 + k \in ℕ_{0}$
78		bccl	$⊢ (N + 1 + k \in ℕ_{0} \land k + 1 \in ℤ) \to (\binom{N + 1 + k}{k + 1}) \in ℕ_{0}$
79	77 70 78	syl2anc	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to (\binom{N + 1 + k}{k + 1}) \in ℕ_{0}$
80	79	nn0cnd	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to (\binom{N + 1 + k}{k + 1}) \in ℂ$
81		nn0z	$⊢ k \in ℕ_{0} \to k \in ℤ$
82	81	adantl	$⊢ (N + 1 \in ℕ_{0} \land k \in ℕ_{0}) \to k \in ℤ$
83		bccl	$⊢ (N + 1 + k \in ℕ_{0} \land k \in ℤ) \to (\binom{N + 1 + k}{k}) \in ℕ_{0}$
84	66 82 83	syl2anc	$⊢ (N + 1 \in ℕ_{0} \land k \in ℕ_{0}) \to (\binom{N + 1 + k}{k}) \in ℕ_{0}$
85	29 84	sylan	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to (\binom{N + 1 + k}{k}) \in ℕ_{0}$
86	85	nn0cnd	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to (\binom{N + 1 + k}{k}) \in ℂ$
87	80 86	addcomd	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to (\binom{N + 1 + k}{k + 1}) + (\binom{N + 1 + k}{k}) = (\binom{N + 1 + k}{k}) + (\binom{N + 1 + k}{k + 1})$
88		peano2cn	$⊢ N \in ℂ \to N + 1 \in ℂ$
89	48 88	syl	$⊢ N \in ℕ_{0} \to N + 1 \in ℂ$
90	89	adantr	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to N + 1 \in ℂ$
91	90 51 52	addassd	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to (N + 1) + k + 1 = N + 1 + k + 1$
92	91	oveq1d	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to (\binom{(N + 1) + k + 1}{k + 1}) = (\binom{N + 1 + k + 1}{k + 1})$
93	73 87 92	3eqtr3d	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to (\binom{N + 1 + k}{k}) + (\binom{N + 1 + k}{k + 1}) = (\binom{N + 1 + k + 1}{k + 1})$
94	93	adantr	$⊢ ((N \in ℕ_{0} \land k \in ℕ_{0}) \land (\binom{N + 1 + k}{k}) = \sum_{j = 0}^{k} (\binom{N + j}{j})) \to (\binom{N + 1 + k}{k}) + (\binom{N + 1 + k}{k + 1}) = (\binom{N + 1 + k + 1}{k + 1})$
95	58 60 94	3eqtr2rd	$⊢ ((N \in ℕ_{0} \land k \in ℕ_{0}) \land (\binom{N + 1 + k}{k}) = \sum_{j = 0}^{k} (\binom{N + j}{j})) \to (\binom{N + 1 + k + 1}{k + 1}) = \sum_{j = 0}^{k + 1} (\binom{N + j}{j})$
96	4 8 12 16 34 95	nn0indd	$⊢ (N \in ℕ_{0} \land M \in ℕ_{0}) \to (\binom{N + 1 + M}{M}) = \sum_{j = 0}^{M} (\binom{N + j}{j})$

Metamath Proof Explorer

Theorem bcxmas

Proof