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		simpr	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to k \in ℕ_{0}$
36		elnn0uz	$⊢ k \in ℕ_{0} \leftrightarrow k \in ℤ_{\geq 0}$
37	35 36	sylib	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to k \in ℤ_{\geq 0}$
38		simpl	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to N \in ℕ_{0}$
39		elfznn0	$⊢ j \in (0 \dots k + 1) \to j \in ℕ_{0}$
40		nn0addcl	$⊢ (N \in ℕ_{0} \land j \in ℕ_{0}) \to N + j \in ℕ_{0}$
41	38 39 40	syl2an	$⊢ ((N \in ℕ_{0} \land k \in ℕ_{0}) \land j \in (0 \dots k + 1)) \to N + j \in ℕ_{0}$
42		elfzelz	$⊢ j \in (0 \dots k + 1) \to j \in ℤ$
43	42	adantl	$⊢ ((N \in ℕ_{0} \land k \in ℕ_{0}) \land j \in (0 \dots k + 1)) \to j \in ℤ$
44		bccl	$⊢ (N + j \in ℕ_{0} \land j \in ℤ) \to (\binom{N + j}{j}) \in ℕ_{0}$
45	41 43 44	syl2anc	$⊢ ((N \in ℕ_{0} \land k \in ℕ_{0}) \land j \in (0 \dots k + 1)) \to (\binom{N + j}{j}) \in ℕ_{0}$
46	45	nn0cnd	$⊢ ((N \in ℕ_{0} \land k \in ℕ_{0}) \land j \in (0 \dots k + 1)) \to (\binom{N + j}{j}) \in ℂ$
47		bcxmaslem1	$⊢ j = k + 1 \to (\binom{N + j}{j}) = (\binom{N + k + 1}{k + 1})$
48	37 46 47	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})$
49		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
50	49	adantr	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to N \in ℂ$
51		nn0cn	$⊢ k \in ℕ_{0} \to k \in ℂ$
52	51	adantl	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to k \in ℂ$
53		1cnd	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to 1 \in ℂ$
54		add32r	$⊢ (N \in ℂ \land k \in ℂ \land 1 \in ℂ) \to N + k + 1 = N + 1 + k$
55	50 52 53 54	syl3anc	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to N + k + 1 = N + 1 + k$
56	55	oveq1d	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to (\binom{N + k + 1}{k + 1}) = (\binom{N + 1 + k}{k + 1})$
57	56	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})$
58	48 57	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})$
59	58	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})$
60		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})$
61	60	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})$
62		ax-1cn	$⊢ 1 \in ℂ$
63		pncan	$⊢ (k \in ℂ \land 1 \in ℂ) \to k + 1 - 1 = k$
64	52 62 63	sylancl	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to k + 1 - 1 = k$
65	64	oveq2d	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to (\binom{N + 1 + k}{k + 1 - 1}) = (\binom{N + 1 + k}{k})$
66	65	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})$
67		nn0addcl	$⊢ (N + 1 \in ℕ_{0} \land k \in ℕ_{0}) \to N + 1 + k \in ℕ_{0}$
68	29 67	sylan	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to N + 1 + k \in ℕ_{0}$
69		nn0p1nn	$⊢ k \in ℕ_{0} \to k + 1 \in ℕ$
70	69	adantl	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to k + 1 \in ℕ$
71	70	nnzd	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to k + 1 \in ℤ$
72		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})$
73	68 71 72	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})$
74	66 73	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})$
75		nn0p1nn	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ$
76		nnnn0addcl	$⊢ (N + 1 \in ℕ \land k \in ℕ_{0}) \to N + 1 + k \in ℕ$
77	75 76	sylan	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to N + 1 + k \in ℕ$
78	77	nnnn0d	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to N + 1 + k \in ℕ_{0}$
79		bccl	$⊢ (N + 1 + k \in ℕ_{0} \land k + 1 \in ℤ) \to (\binom{N + 1 + k}{k + 1}) \in ℕ_{0}$
80	78 71 79	syl2anc	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to (\binom{N + 1 + k}{k + 1}) \in ℕ_{0}$
81	80	nn0cnd	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to (\binom{N + 1 + k}{k + 1}) \in ℂ$
82		nn0z	$⊢ k \in ℕ_{0} \to k \in ℤ$
83	82	adantl	$⊢ (N + 1 \in ℕ_{0} \land k \in ℕ_{0}) \to k \in ℤ$
84		bccl	$⊢ (N + 1 + k \in ℕ_{0} \land k \in ℤ) \to (\binom{N + 1 + k}{k}) \in ℕ_{0}$
85	67 83 84	syl2anc	$⊢ (N + 1 \in ℕ_{0} \land k \in ℕ_{0}) \to (\binom{N + 1 + k}{k}) \in ℕ_{0}$
86	29 85	sylan	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to (\binom{N + 1 + k}{k}) \in ℕ_{0}$
87	86	nn0cnd	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to (\binom{N + 1 + k}{k}) \in ℂ$
88	81 87	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})$
89		peano2cn	$⊢ N \in ℂ \to N + 1 \in ℂ$
90	49 89	syl	$⊢ N \in ℕ_{0} \to N + 1 \in ℂ$
91	90	adantr	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to N + 1 \in ℂ$
92	91 52 53	addassd	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to (N + 1) + k + 1 = N + 1 + k + 1$
93	92	oveq1d	$⊢ (N \in ℕ_{0} \land k \in ℕ_{0}) \to (\binom{(N + 1) + k + 1}{k + 1}) = (\binom{N + 1 + k + 1}{k + 1})$
94	74 88 93	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})$
95	94	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})$
96	59 61 95	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})$
97	4 8 12 16 34 96	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