bcpasc

Description: Pascal's rule for the binomial coefficient, generalized to all integers K . Equation 2 of Gleason p. 295. (Contributed by NM, 13-Jul-2005) (Revised by Mario Carneiro, 10-Mar-2014)

		Ref	Expression
	Assertion	bcpasc	$⊢ (N \in ℕ_{0} \land K \in ℤ) \to (\binom{N}{K}) + (\binom{N}{K - 1}) = (\binom{N + 1}{K})$

Proof

Step	Hyp	Ref	Expression
1		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
2		elfzp12	$⊢ N + 1 \in ℤ_{\geq 0} \to (K \in (0 \dots N + 1) \leftrightarrow (K = 0 \lor K \in (0 + 1 \dots N + 1)))$
3		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
4	2 3	eleq2s	$⊢ N + 1 \in ℕ_{0} \to (K \in (0 \dots N + 1) \leftrightarrow (K = 0 \lor K \in (0 + 1 \dots N + 1)))$
5	1 4	syl	$⊢ N \in ℕ_{0} \to (K \in (0 \dots N + 1) \leftrightarrow (K = 0 \lor K \in (0 + 1 \dots N + 1)))$
6		1p0e1	$⊢ 1 + 0 = 1$
7		bcn0	$⊢ N \in ℕ_{0} \to (\binom{N}{0}) = 1$
8		0z	$⊢ 0 \in ℤ$
9		1z	$⊢ 1 \in ℤ$
10		zsubcl	$⊢ (0 \in ℤ \land 1 \in ℤ) \to 0 - 1 \in ℤ$
11	8 9 10	mp2an	$⊢ 0 - 1 \in ℤ$
12		0re	$⊢ 0 \in ℝ$
13		ltm1	$⊢ 0 \in ℝ \to 0 - 1 < 0$
14	12 13	ax-mp	$⊢ 0 - 1 < 0$
15	14	orci	$⊢ (0 - 1 < 0 \lor N < 0 - 1)$
16		bcval4	$⊢ (N \in ℕ_{0} \land 0 - 1 \in ℤ \land (0 - 1 < 0 \lor N < 0 - 1)) \to (\binom{N}{0 - 1}) = 0$
17	11 15 16	mp3an23	$⊢ N \in ℕ_{0} \to (\binom{N}{0 - 1}) = 0$
18	7 17	oveq12d	$⊢ N \in ℕ_{0} \to (\binom{N}{0}) + (\binom{N}{0 - 1}) = 1 + 0$
19		bcn0	$⊢ N + 1 \in ℕ_{0} \to (\binom{N + 1}{0}) = 1$
20	1 19	syl	$⊢ N \in ℕ_{0} \to (\binom{N + 1}{0}) = 1$
21	6 18 20	3eqtr4a	$⊢ N \in ℕ_{0} \to (\binom{N}{0}) + (\binom{N}{0 - 1}) = (\binom{N + 1}{0})$
22		oveq2	$⊢ K = 0 \to (\binom{N}{K}) = (\binom{N}{0})$
23		oveq1	$⊢ K = 0 \to K - 1 = 0 - 1$
24	23	oveq2d	$⊢ K = 0 \to (\binom{N}{K - 1}) = (\binom{N}{0 - 1})$
25	22 24	oveq12d	$⊢ K = 0 \to (\binom{N}{K}) + (\binom{N}{K - 1}) = (\binom{N}{0}) + (\binom{N}{0 - 1})$
26		oveq2	$⊢ K = 0 \to (\binom{N + 1}{K}) = (\binom{N + 1}{0})$
27	25 26	eqeq12d	$⊢ K = 0 \to ((\binom{N}{K}) + (\binom{N}{K - 1}) = (\binom{N + 1}{K}) \leftrightarrow (\binom{N}{0}) + (\binom{N}{0 - 1}) = (\binom{N + 1}{0}))$
28	21 27	syl5ibrcom	$⊢ N \in ℕ_{0} \to (K = 0 \to (\binom{N}{K}) + (\binom{N}{K - 1}) = (\binom{N + 1}{K}))$
29		simpr	$⊢ (N \in ℕ_{0} \land K \in (0 + 1 \dots N + 1)) \to K \in (0 + 1 \dots N + 1)$
30		0p1e1	$⊢ 0 + 1 = 1$
31	30	oveq1i	$⊢ (0 + 1 \dots N + 1) = (1 \dots N + 1)$
32	29 31	eleqtrdi	$⊢ (N \in ℕ_{0} \land K \in (0 + 1 \dots N + 1)) \to K \in (1 \dots N + 1)$
33		nn0p1nn	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ$
34		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
35	33 34	eleqtrdi	$⊢ N \in ℕ_{0} \to N + 1 \in ℤ_{\geq 1}$
36		fzm1	$⊢ N + 1 \in ℤ_{\geq 1} \to (K \in (1 \dots N + 1) \leftrightarrow (K \in (1 \dots N + 1 - 1) \lor K = N + 1))$
37	36	biimpa	$⊢ (N + 1 \in ℤ_{\geq 1} \land K \in (1 \dots N + 1)) \to (K \in (1 \dots N + 1 - 1) \lor K = N + 1)$
38	35 37	sylan	$⊢ (N \in ℕ_{0} \land K \in (1 \dots N + 1)) \to (K \in (1 \dots N + 1 - 1) \lor K = N + 1)$
39		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
40		ax-1cn	$⊢ 1 \in ℂ$
41		pncan	$⊢ (N \in ℂ \land 1 \in ℂ) \to N + 1 - 1 = N$
42	39 40 41	sylancl	$⊢ N \in ℕ_{0} \to N + 1 - 1 = N$
43	42	oveq2d	$⊢ N \in ℕ_{0} \to (1 \dots N + 1 - 1) = (1 \dots N)$
44	43	eleq2d	$⊢ N \in ℕ_{0} \to (K \in (1 \dots N + 1 - 1) \leftrightarrow K \in (1 \dots N))$
45	44	biimpa	$⊢ (N \in ℕ_{0} \land K \in (1 \dots N + 1 - 1)) \to K \in (1 \dots N)$
46		fz1ssfz0	$⊢ (1 \dots N) \subseteq (0 \dots N)$
47	46	sseli	$⊢ K \in (1 \dots N) \to K \in (0 \dots N)$
48		bcp1n	$⊢ K \in (0 \dots N) \to (\binom{N + 1}{K}) = (\binom{N}{K}) (\frac{N + 1}{N + 1 - K})$
49	47 48	syl	$⊢ K \in (1 \dots N) \to (\binom{N + 1}{K}) = (\binom{N}{K}) (\frac{N + 1}{N + 1 - K})$
50		bcrpcl	$⊢ K \in (0 \dots N) \to (\binom{N}{K}) \in ℝ^{+}$
51	47 50	syl	$⊢ K \in (1 \dots N) \to (\binom{N}{K}) \in ℝ^{+}$
52	51	rpcnd	$⊢ K \in (1 \dots N) \to (\binom{N}{K}) \in ℂ$
53		elfzuz2	$⊢ K \in (1 \dots N) \to N \in ℤ_{\geq 1}$
54	53 34	eleqtrrdi	$⊢ K \in (1 \dots N) \to N \in ℕ$
55	54	peano2nnd	$⊢ K \in (1 \dots N) \to N + 1 \in ℕ$
56	55	nncnd	$⊢ K \in (1 \dots N) \to N + 1 \in ℂ$
57	54	nncnd	$⊢ K \in (1 \dots N) \to N \in ℂ$
58		1cnd	$⊢ K \in (1 \dots N) \to 1 \in ℂ$
59		elfzelz	$⊢ K \in (1 \dots N) \to K \in ℤ$
60	59	zcnd	$⊢ K \in (1 \dots N) \to K \in ℂ$
61	57 58 60	addsubd	$⊢ K \in (1 \dots N) \to N + 1 - K = N - K + 1$
62		fznn0sub	$⊢ K \in (1 \dots N) \to N - K \in ℕ_{0}$
63		nn0p1nn	$⊢ N - K \in ℕ_{0} \to N - K + 1 \in ℕ$
64	62 63	syl	$⊢ K \in (1 \dots N) \to N - K + 1 \in ℕ$
65	61 64	eqeltrd	$⊢ K \in (1 \dots N) \to N + 1 - K \in ℕ$
66	65	nncnd	$⊢ K \in (1 \dots N) \to N + 1 - K \in ℂ$
67	65	nnne0d	$⊢ K \in (1 \dots N) \to N + 1 - K \neq 0$
68	52 56 66 67	div12d	$⊢ K \in (1 \dots N) \to (\binom{N}{K}) (\frac{N + 1}{N + 1 - K}) = (N + 1) (\frac{(\binom{N}{K})}{N + 1 - K})$
69	65	nnrpd	$⊢ K \in (1 \dots N) \to N + 1 - K \in ℝ^{+}$
70	51 69	rpdivcld	$⊢ K \in (1 \dots N) \to \frac{(\binom{N}{K})}{N + 1 - K} \in ℝ^{+}$
71	70	rpcnd	$⊢ K \in (1 \dots N) \to \frac{(\binom{N}{K})}{N + 1 - K} \in ℂ$
72	56 71	mulcomd	$⊢ K \in (1 \dots N) \to (N + 1) (\frac{(\binom{N}{K})}{N + 1 - K}) = (\frac{(\binom{N}{K})}{N + 1 - K}) (N + 1)$
73	68 72	eqtrd	$⊢ K \in (1 \dots N) \to (\binom{N}{K}) (\frac{N + 1}{N + 1 - K}) = (\frac{(\binom{N}{K})}{N + 1 - K}) (N + 1)$
74	56 60	npcand	$⊢ K \in (1 \dots N) \to (N + 1) - K + K = N + 1$
75	74	oveq2d	$⊢ K \in (1 \dots N) \to (\frac{(\binom{N}{K})}{N + 1 - K}) ((N + 1) - K + K) = (\frac{(\binom{N}{K})}{N + 1 - K}) (N + 1)$
76	71 66 60	adddid	$⊢ K \in (1 \dots N) \to (\frac{(\binom{N}{K})}{N + 1 - K}) ((N + 1) - K + K) = (\frac{(\binom{N}{K})}{N + 1 - K}) (N + 1 - K) + (\frac{(\binom{N}{K})}{N + 1 - K}) K$
77	73 75 76	3eqtr2d	$⊢ K \in (1 \dots N) \to (\binom{N}{K}) (\frac{N + 1}{N + 1 - K}) = (\frac{(\binom{N}{K})}{N + 1 - K}) (N + 1 - K) + (\frac{(\binom{N}{K})}{N + 1 - K}) K$
78	52 66 67	divcan1d	$⊢ K \in (1 \dots N) \to (\frac{(\binom{N}{K})}{N + 1 - K}) (N + 1 - K) = (\binom{N}{K})$
79		elfznn	$⊢ K \in (1 \dots N) \to K \in ℕ$
80	79	nnne0d	$⊢ K \in (1 \dots N) \to K \neq 0$
81	52 66 60 67 80	divdiv2d	$⊢ K \in (1 \dots N) \to \frac{(\binom{N}{K})}{\frac{N + 1 - K}{K}} = \frac{(\binom{N}{K}) K}{N + 1 - K}$
82		bcm1k	$⊢ K \in (1 \dots N) \to (\binom{N}{K}) = (\binom{N}{K - 1}) (\frac{N - (K - 1)}{K})$
83	57 60 58	subsub3d	$⊢ K \in (1 \dots N) \to N - (K - 1) = N + 1 - K$
84	83	oveq1d	$⊢ K \in (1 \dots N) \to \frac{N - (K - 1)}{K} = \frac{N + 1 - K}{K}$
85	84	oveq2d	$⊢ K \in (1 \dots N) \to (\binom{N}{K - 1}) (\frac{N - (K - 1)}{K}) = (\binom{N}{K - 1}) (\frac{N + 1 - K}{K})$
86	82 85	eqtrd	$⊢ K \in (1 \dots N) \to (\binom{N}{K}) = (\binom{N}{K - 1}) (\frac{N + 1 - K}{K})$
87		fzelp1	$⊢ K \in (1 \dots N) \to K \in (1 \dots N + 1)$
88	55	nnzd	$⊢ K \in (1 \dots N) \to N + 1 \in ℤ$
89		elfzm1b	$⊢ (K \in ℤ \land N + 1 \in ℤ) \to (K \in (1 \dots N + 1) \leftrightarrow K - 1 \in (0 \dots N + 1 - 1))$
90	59 88 89	syl2anc	$⊢ K \in (1 \dots N) \to (K \in (1 \dots N + 1) \leftrightarrow K - 1 \in (0 \dots N + 1 - 1))$
91	87 90	mpbid	$⊢ K \in (1 \dots N) \to K - 1 \in (0 \dots N + 1 - 1)$
92	57 40 41	sylancl	$⊢ K \in (1 \dots N) \to N + 1 - 1 = N$
93	92	oveq2d	$⊢ K \in (1 \dots N) \to (0 \dots N + 1 - 1) = (0 \dots N)$
94	91 93	eleqtrd	$⊢ K \in (1 \dots N) \to K - 1 \in (0 \dots N)$
95		bcrpcl	$⊢ K - 1 \in (0 \dots N) \to (\binom{N}{K - 1}) \in ℝ^{+}$
96	94 95	syl	$⊢ K \in (1 \dots N) \to (\binom{N}{K - 1}) \in ℝ^{+}$
97	96	rpcnd	$⊢ K \in (1 \dots N) \to (\binom{N}{K - 1}) \in ℂ$
98	79	nnrpd	$⊢ K \in (1 \dots N) \to K \in ℝ^{+}$
99	69 98	rpdivcld	$⊢ K \in (1 \dots N) \to \frac{N + 1 - K}{K} \in ℝ^{+}$
100	99	rpcnd	$⊢ K \in (1 \dots N) \to \frac{N + 1 - K}{K} \in ℂ$
101	99	rpne0d	$⊢ K \in (1 \dots N) \to \frac{N + 1 - K}{K} \neq 0$
102	52 97 100 101	divmul3d	$⊢ K \in (1 \dots N) \to (\frac{(\binom{N}{K})}{\frac{N + 1 - K}{K}} = (\binom{N}{K - 1}) \leftrightarrow (\binom{N}{K}) = (\binom{N}{K - 1}) (\frac{N + 1 - K}{K}))$
103	86 102	mpbird	$⊢ K \in (1 \dots N) \to \frac{(\binom{N}{K})}{\frac{N + 1 - K}{K}} = (\binom{N}{K - 1})$
104	52 60 66 67	div23d	$⊢ K \in (1 \dots N) \to \frac{(\binom{N}{K}) K}{N + 1 - K} = (\frac{(\binom{N}{K})}{N + 1 - K}) K$
105	81 103 104	3eqtr3rd	$⊢ K \in (1 \dots N) \to (\frac{(\binom{N}{K})}{N + 1 - K}) K = (\binom{N}{K - 1})$
106	78 105	oveq12d	$⊢ K \in (1 \dots N) \to (\frac{(\binom{N}{K})}{N + 1 - K}) (N + 1 - K) + (\frac{(\binom{N}{K})}{N + 1 - K}) K = (\binom{N}{K}) + (\binom{N}{K - 1})$
107	49 77 106	3eqtrrd	$⊢ K \in (1 \dots N) \to (\binom{N}{K}) + (\binom{N}{K - 1}) = (\binom{N + 1}{K})$
108	45 107	syl	$⊢ (N \in ℕ_{0} \land K \in (1 \dots N + 1 - 1)) \to (\binom{N}{K}) + (\binom{N}{K - 1}) = (\binom{N + 1}{K})$
109		oveq2	$⊢ K = N + 1 \to (\binom{N}{K}) = (\binom{N}{N + 1})$
110	33	nnzd	$⊢ N \in ℕ_{0} \to N + 1 \in ℤ$
111		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
112	111	ltp1d	$⊢ N \in ℕ_{0} \to N < N + 1$
113	112	olcd	$⊢ N \in ℕ_{0} \to (N + 1 < 0 \lor N < N + 1)$
114		bcval4	$⊢ (N \in ℕ_{0} \land N + 1 \in ℤ \land (N + 1 < 0 \lor N < N + 1)) \to (\binom{N}{N + 1}) = 0$
115	110 113 114	mpd3an23	$⊢ N \in ℕ_{0} \to (\binom{N}{N + 1}) = 0$
116	109 115	sylan9eqr	$⊢ (N \in ℕ_{0} \land K = N + 1) \to (\binom{N}{K}) = 0$
117		oveq1	$⊢ K = N + 1 \to K - 1 = N + 1 - 1$
118	117 42	sylan9eqr	$⊢ (N \in ℕ_{0} \land K = N + 1) \to K - 1 = N$
119	118	oveq2d	$⊢ (N \in ℕ_{0} \land K = N + 1) \to (\binom{N}{K - 1}) = (\binom{N}{N})$
120		bcnn	$⊢ N \in ℕ_{0} \to (\binom{N}{N}) = 1$
121	120	adantr	$⊢ (N \in ℕ_{0} \land K = N + 1) \to (\binom{N}{N}) = 1$
122	119 121	eqtrd	$⊢ (N \in ℕ_{0} \land K = N + 1) \to (\binom{N}{K - 1}) = 1$
123	116 122	oveq12d	$⊢ (N \in ℕ_{0} \land K = N + 1) \to (\binom{N}{K}) + (\binom{N}{K - 1}) = 0 + 1$
124		oveq2	$⊢ K = N + 1 \to (\binom{N + 1}{K}) = (\binom{N + 1}{N + 1})$
125		bcnn	$⊢ N + 1 \in ℕ_{0} \to (\binom{N + 1}{N + 1}) = 1$
126	1 125	syl	$⊢ N \in ℕ_{0} \to (\binom{N + 1}{N + 1}) = 1$
127	124 126	sylan9eqr	$⊢ (N \in ℕ_{0} \land K = N + 1) \to (\binom{N + 1}{K}) = 1$
128	30 123 127	3eqtr4a	$⊢ (N \in ℕ_{0} \land K = N + 1) \to (\binom{N}{K}) + (\binom{N}{K - 1}) = (\binom{N + 1}{K})$
129	108 128	jaodan	$⊢ (N \in ℕ_{0} \land (K \in (1 \dots N + 1 - 1) \lor K = N + 1)) \to (\binom{N}{K}) + (\binom{N}{K - 1}) = (\binom{N + 1}{K})$
130	38 129	syldan	$⊢ (N \in ℕ_{0} \land K \in (1 \dots N + 1)) \to (\binom{N}{K}) + (\binom{N}{K - 1}) = (\binom{N + 1}{K})$
131	32 130	syldan	$⊢ (N \in ℕ_{0} \land K \in (0 + 1 \dots N + 1)) \to (\binom{N}{K}) + (\binom{N}{K - 1}) = (\binom{N + 1}{K})$
132	131	ex	$⊢ N \in ℕ_{0} \to (K \in (0 + 1 \dots N + 1) \to (\binom{N}{K}) + (\binom{N}{K - 1}) = (\binom{N + 1}{K}))$
133	28 132	jaod	$⊢ N \in ℕ_{0} \to ((K = 0 \lor K \in (0 + 1 \dots N + 1)) \to (\binom{N}{K}) + (\binom{N}{K - 1}) = (\binom{N + 1}{K}))$
134	5 133	sylbid	$⊢ N \in ℕ_{0} \to (K \in (0 \dots N + 1) \to (\binom{N}{K}) + (\binom{N}{K - 1}) = (\binom{N + 1}{K}))$
135	134	imp	$⊢ (N \in ℕ_{0} \land K \in (0 \dots N + 1)) \to (\binom{N}{K}) + (\binom{N}{K - 1}) = (\binom{N + 1}{K})$
136	135	adantlr	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land K \in (0 \dots N + 1)) \to (\binom{N}{K}) + (\binom{N}{K - 1}) = (\binom{N + 1}{K})$
137		00id	$⊢ 0 + 0 = 0$
138		fzelp1	$⊢ K \in (0 \dots N) \to K \in (0 \dots N + 1)$
139	138	con3i	$⊢ \neg K \in (0 \dots N + 1) \to \neg K \in (0 \dots N)$
140		bcval3	$⊢ (N \in ℕ_{0} \land K \in ℤ \land \neg K \in (0 \dots N)) \to (\binom{N}{K}) = 0$
141	140	3expa	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land \neg K \in (0 \dots N)) \to (\binom{N}{K}) = 0$
142	139 141	sylan2	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land \neg K \in (0 \dots N + 1)) \to (\binom{N}{K}) = 0$
143		simpll	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land \neg K \in (0 \dots N + 1)) \to N \in ℕ_{0}$
144		simplr	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land \neg K \in (0 \dots N + 1)) \to K \in ℤ$
145		peano2zm	$⊢ K \in ℤ \to K - 1 \in ℤ$
146	144 145	syl	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land \neg K \in (0 \dots N + 1)) \to K - 1 \in ℤ$
147	39	adantr	$⊢ (N \in ℕ_{0} \land K \in ℤ) \to N \in ℂ$
148	147 40 41	sylancl	$⊢ (N \in ℕ_{0} \land K \in ℤ) \to N + 1 - 1 = N$
149	148	oveq2d	$⊢ (N \in ℕ_{0} \land K \in ℤ) \to (0 \dots N + 1 - 1) = (0 \dots N)$
150	149	eleq2d	$⊢ (N \in ℕ_{0} \land K \in ℤ) \to (K - 1 \in (0 \dots N + 1 - 1) \leftrightarrow K - 1 \in (0 \dots N))$
151		id	$⊢ K \in ℤ \to K \in ℤ$
152	1	nn0zd	$⊢ N \in ℕ_{0} \to N + 1 \in ℤ$
153	151 152 89	syl2anr	$⊢ (N \in ℕ_{0} \land K \in ℤ) \to (K \in (1 \dots N + 1) \leftrightarrow K - 1 \in (0 \dots N + 1 - 1))$
154		fz1ssfz0	$⊢ (1 \dots N + 1) \subseteq (0 \dots N + 1)$
155	154	sseli	$⊢ K \in (1 \dots N + 1) \to K \in (0 \dots N + 1)$
156	153 155	syl6bir	$⊢ (N \in ℕ_{0} \land K \in ℤ) \to (K - 1 \in (0 \dots N + 1 - 1) \to K \in (0 \dots N + 1))$
157	150 156	sylbird	$⊢ (N \in ℕ_{0} \land K \in ℤ) \to (K - 1 \in (0 \dots N) \to K \in (0 \dots N + 1))$
158	157	con3dimp	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land \neg K \in (0 \dots N + 1)) \to \neg K - 1 \in (0 \dots N)$
159		bcval3	$⊢ (N \in ℕ_{0} \land K - 1 \in ℤ \land \neg K - 1 \in (0 \dots N)) \to (\binom{N}{K - 1}) = 0$
160	143 146 158 159	syl3anc	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land \neg K \in (0 \dots N + 1)) \to (\binom{N}{K - 1}) = 0$
161	142 160	oveq12d	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land \neg K \in (0 \dots N + 1)) \to (\binom{N}{K}) + (\binom{N}{K - 1}) = 0 + 0$
162	143 1	syl	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land \neg K \in (0 \dots N + 1)) \to N + 1 \in ℕ_{0}$
163		simpr	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land \neg K \in (0 \dots N + 1)) \to \neg K \in (0 \dots N + 1)$
164		bcval3	$⊢ (N + 1 \in ℕ_{0} \land K \in ℤ \land \neg K \in (0 \dots N + 1)) \to (\binom{N + 1}{K}) = 0$
165	162 144 163 164	syl3anc	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land \neg K \in (0 \dots N + 1)) \to (\binom{N + 1}{K}) = 0$
166	137 161 165	3eqtr4a	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land \neg K \in (0 \dots N + 1)) \to (\binom{N}{K}) + (\binom{N}{K - 1}) = (\binom{N + 1}{K})$
167	136 166	pm2.61dan	$⊢ (N \in ℕ_{0} \land K \in ℤ) \to (\binom{N}{K}) + (\binom{N}{K - 1}) = (\binom{N + 1}{K})$

Metamath Proof Explorer

Theorem bcpasc

Proof