Definition df-bc 12071

Description: Define the binomial coefficient operation. 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 12070	. 2 class _C
2		vn	. . 3 setvar n
3		vk	. . 3 setvar k
4		cn0 10571	. . 3 class NN0
5		cz 10638	. . 3 class ZZ
6	3	cv 1368	. . . . 5 class k
7		cc0 9274	. . . . . 6 class 0
8	2	cv 1368	. . . . . 6 class n
9		cfz 11429	. . . . . 6 class ...
10	7, 8, 9	co 6086	. . . . 5 class ( 0 ... n )
11	6, 10	wcel 1756	. . . 4 wff k e. ( 0 ... n )
12		cfa 12043	. . . . . 6 class !
13	8, 12	cfv 5413	. . . . 5 class ( ! ` n )
14		cmin 9587	. . . . . . . 8 class -
15	8, 6, 14	co 6086	. . . . . . 7 class ( n - k )
16	15, 12	cfv 5413	. . . . . 6 class ( ! ` ( n - k ) )
17	6, 12	cfv 5413	. . . . . 6 class ( ! ` k )
18		cmul 9279	. . . . . 6 class x.
19	16, 17, 18	co 6086	. . . . 5 class ( ( ! ` ( n - k ) ) x. ( ! ` k ) )
20		cdiv 9985	. . . . 5 class /
21	13, 19, 20	co 6086	. . . 4 class ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) )
22	11, 21, 7	cif 3786	. . 3 class if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 )
23	2, 3, 4, 5, 22	cmpt2 6088	. 2 class ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) )
24	1, 23	wceq 1369	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  12072