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	|- _C = ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cbc	|- _C
1		vn	|- n
2		cn0	|- NN0
3		vk	|- k
4		cz	|- ZZ
5	3	cv	|- k
6		cc0	|- 0
7		cfz	|- ...
8	1	cv	|- n
9	6 8 7	co	|- ( 0 ... n )
10	5 9	wcel	|- k e. ( 0 ... n )
11		cfa	|- !
12	8 11	cfv	|- ( ! ` n )
13		cdiv	|- /
14		cmin	|- -
15	8 5 14	co	|- ( n - k )
16	15 11	cfv	|- ( ! ` ( n - k ) )
17		cmul	|- x.
18	5 11	cfv	|- ( ! ` k )
19	16 18 17	co	|- ( ( ! ` ( n - k ) ) x. ( ! ` k ) )
20	12 19 13	co	|- ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) )
21	10 20 6	cif	|- if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 )
22	1 3 2 4 21	cmpo	|- ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) )
23	0 22	wceq	|- _C = ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) )