Definition df-bc

Description: Define the binomial coefficient operation. For example, ( 5C 3 ) = 1 0 ( ex-bc ).

In the literature, this function is often written as a column vector of the two arguments, or with the arguments as subscripts before and after the letter "C". The expression ( N C K ) is read " N choose K ". Definition of binomial coefficient in Gleason p. 295. As suggested by Gleason, we define it to be 0 when 0 <_ k <_ n does not hold. (Contributed by NM, 10-Jul-2005)

	Ref	Expression
Assertion	df-bc	$$⊢\left(\genfrac{}{}{0ex}{}{.}{.}\right)=\left(n\in {\mathbb{N}}_0,k\in \mathbb{Z}⟼if\left(k\in \left(0\dots n\right),\frac{n!}{\left(n-k\right)!k!},0\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cbc	$$class\left(\genfrac{}{}{0ex}{}{.}{.}\right)$$
1		vn	$$setvarn$$
2		cn0	$$class{\mathbb{N}}_0$$
3		vk	$$setvark$$
4		cz	$$class\mathbb{Z}$$
5	3	cv	$$setvark$$
6		cc0	$$class0$$
7		cfz	$$class\dots$$
8	1	cv	$$setvarn$$
9	6 8 7	co	$$class\left(0\dots n\right)$$
10	5 9	wcel	$$wffk\in \left(0\dots n\right)$$
11		cfa	$$class!$$
12	8 11	cfv	$$classn!$$
13		cdiv	$$class÷$$
14		cmin	$$class-$$
15	8 5 14	co	$$class\left(n-k\right)$$
16	15 11	cfv	$$class\left(n-k\right)!$$
17		cmul	$$class\times$$
18	5 11	cfv	$$classk!$$
19	16 18 17	co	$$class\left(n-k\right)!k!$$
20	12 19 13	co	$$class\left(\frac{n!}{\left(n-k\right)!k!}\right)$$
21	10 20 6	cif	$$classif\left(k\in \left(0\dots n\right),\frac{n!}{\left(n-k\right)!k!},0\right)$$
22	1 3 2 4 21	cmpo	$$class\left(n\in {\mathbb{N}}_0,k\in \mathbb{Z}⟼if\left(k\in \left(0\dots n\right),\frac{n!}{\left(n-k\right)!k!},0\right)\right)$$
23	0 22	wceq	$$wff\left(\genfrac{}{}{0ex}{}{.}{.}\right)=\left(n\in {\mathbb{N}}_0,k\in \mathbb{Z}⟼if\left(k\in \left(0\dots n\right),\frac{n!}{\left(n-k\right)!k!},0\right)\right)$$