Definition df-bc 10730

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

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". ( 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.)

Assertion

Ref	Expression
df-bc	|- _C = ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) )

Distinct variable group:   k, n

Detailed syntax breakdown of Definition df-bc

Step	Hyp	Ref	Expression
1		cbc 10729	. 2 class _C
2		vn	. . 3 setvar n
3		vk	. . 3 setvar k
4		cn0 9178	. . 3 class NN0
5		cz 9255	. . 3 class ZZ
6	3	cv 1352	. . . . 5 class k
7		cc0 7813	. . . . . 6 class 0
8	2	cv 1352	. . . . . 6 class n
9		cfz 10010	. . . . . 6 class ...
10	7, 8, 9	co 5877	. . . . 5 class ( 0 ... n )
11	6, 10	wcel 2148	. . . 4 wff k e. ( 0 ... n )
12		cfa 10707	. . . . . 6 class !
13	8, 12	cfv 5218	. . . . 5 class ( ! ` n )
14		cmin 8130	. . . . . . . 8 class -
15	8, 6, 14	co 5877	. . . . . . 7 class ( n - k )
16	15, 12	cfv 5218	. . . . . 6 class ( ! ` ( n - k ) )
17	6, 12	cfv 5218	. . . . . 6 class ( ! ` k )
18		cmul 7818	. . . . . 6 class x.
19	16, 17, 18	co 5877	. . . . 5 class ( ( ! ` ( n - k ) ) x. ( ! ` k ) )
20		cdiv 8631	. . . . 5 class /
21	13, 19, 20	co 5877	. . . 4 class ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) )
22	11, 21, 7	cif 3536	. . 3 class if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 )
23	2, 3, 4, 5, 22	cmpo 5879	. 2 class ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) )
24	1, 23	wceq 1353	1 wff _C = ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) )

This definition is referenced by:  bcval  10731