Definition df-bc 11549

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 11548	. 2 class _C
2		vn	. . 3 set n
3		vk	. . 3 set k
4		cn0 10177	. . 3 class NN0
5		cz 10238	. . 3 class ZZ
6	3	cv 1648	. . . . 5 class k
7		cc0 8946	. . . . . 6 class 0
8	2	cv 1648	. . . . . 6 class n
9		cfz 10999	. . . . . 6 class ...
10	7, 8, 9	co 6040	. . . . 5 class ( 0 ... n )
11	6, 10	wcel 1721	. . . 4 wff k e. ( 0 ... n )
12		cfa 11521	. . . . . 6 class !
13	8, 12	cfv 5413	. . . . 5 class ( ! ` n )
14		cmin 9247	. . . . . . . 8 class -
15	8, 6, 14	co 6040	. . . . . . 7 class ( n - k )
16	15, 12	cfv 5413	. . . . . 6 class ( ! ` ( n - k ) )
17	6, 12	cfv 5413	. . . . . 6 class ( ! ` k )
18		cmul 8951	. . . . . 6 class x.
19	16, 17, 18	co 6040	. . . . 5 class ( ( ! ` ( n - k ) ) x. ( ! ` k ) )
20		cdiv 9633	. . . . 5 class /
21	13, 19, 20	co 6040	. . . 4 class ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) )
22	11, 21, 7	cif 3699	. . 3 class if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 )
23	2, 3, 4, 5, 22	cmpt2 6042	. 2 class ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) )
24	1, 23	wceq 1649	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  11550