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 = ( 𝑛 ∈ ℕ0 , 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ ( 0 ... 𝑛 ) , ( ( ! ‘ 𝑛 ) / ( ( ! ‘ ( 𝑛 − 𝑘 ) ) · ( ! ‘ 𝑘 ) ) ) , 0 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cbc	⊢ C
1		vn	⊢ 𝑛
2		cn0	⊢ ℕ0
3		vk	⊢ 𝑘
4		cz	⊢ ℤ
5	3	cv	⊢ 𝑘
6		cc0	⊢ 0
7		cfz	⊢ ...
8	1	cv	⊢ 𝑛
9	6 8 7	co	⊢ ( 0 ... 𝑛 )
10	5 9	wcel	⊢ 𝑘 ∈ ( 0 ... 𝑛 )
11		cfa	⊢ !
12	8 11	cfv	⊢ ( ! ‘ 𝑛 )
13		cdiv	⊢ /
14		cmin	⊢ −
15	8 5 14	co	⊢ ( 𝑛 − 𝑘 )
16	15 11	cfv	⊢ ( ! ‘ ( 𝑛 − 𝑘 ) )
17		cmul	⊢ ·
18	5 11	cfv	⊢ ( ! ‘ 𝑘 )
19	16 18 17	co	⊢ ( ( ! ‘ ( 𝑛 − 𝑘 ) ) · ( ! ‘ 𝑘 ) )
20	12 19 13	co	⊢ ( ( ! ‘ 𝑛 ) / ( ( ! ‘ ( 𝑛 − 𝑘 ) ) · ( ! ‘ 𝑘 ) ) )
21	10 20 6	cif	⊢ if ( 𝑘 ∈ ( 0 ... 𝑛 ) , ( ( ! ‘ 𝑛 ) / ( ( ! ‘ ( 𝑛 − 𝑘 ) ) · ( ! ‘ 𝑘 ) ) ) , 0 )
22	1 3 2 4 21	cmpo	⊢ ( 𝑛 ∈ ℕ0 , 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ ( 0 ... 𝑛 ) , ( ( ! ‘ 𝑛 ) / ( ( ! ‘ ( 𝑛 − 𝑘 ) ) · ( ! ‘ 𝑘 ) ) ) , 0 ) )
23	0 22	wceq	⊢ C = ( 𝑛 ∈ ℕ0 , 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ ( 0 ... 𝑛 ) , ( ( ! ‘ 𝑛 ) / ( ( ! ‘ ( 𝑛 − 𝑘 ) ) · ( ! ‘ 𝑘 ) ) ) , 0 ) )