Definition df-bc 14335

Description: Define the binomial coefficient operation. For example, (5C3) = 10 (ex-bc 30803).

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 (𝑁C𝐾) is read "𝑁 choose 𝐾". Definition of binomial coefficient in [Gleason] p. 295. As suggested by Gleason, we define it to be 0 when 0 ≤ 𝑘 ≤ 𝑛 does not hold. (Contributed by NM, 10-Jul-2005.)

Assertion

Ref	Expression
df-bc	⊢ C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))

Distinct variable group:   𝑘,𝑛

Detailed syntax breakdown of Definition df-bc

Step	Hyp	Ref	Expression
1		cbc 14334	. 2 class C
2		vn	. . 3 setvar 𝑛
3		vk	. . 3 setvar 𝑘
4		cn0 12499	. . 3 class ℕ0
5		cz 12586	. . 3 class ℤ
6	3	cv 1569	. . . . 5 class 𝑘
7		cc0 11095	. . . . . 6 class 0
8	2	cv 1569	. . . . . 6 class 𝑛
9		cfz 13530	. . . . . 6 class ...
10	7, 8, 9	co 7410	. . . . 5 class (0...𝑛)
11	6, 10	wcel 2143	. . . 4 wff 𝑘 ∈ (0...𝑛)
12		cfa 14305	. . . . . 6 class !
13	8, 12	cfv 6536	. . . . 5 class (!‘𝑛)
14		cmin 11436	. . . . . . . 8 class −
15	8, 6, 14	co 7410	. . . . . . 7 class (𝑛 − 𝑘)
16	15, 12	cfv 6536	. . . . . 6 class (!‘(𝑛 − 𝑘))
17	6, 12	cfv 6536	. . . . . 6 class (!‘𝑘)
18		cmul 11100	. . . . . 6 class ·
19	16, 17, 18	co 7410	. . . . 5 class ((!‘(𝑛 − 𝑘)) · (!‘𝑘))
20		cdiv 11866	. . . . 5 class /
21	13, 19, 20	co 7410	. . . 4 class ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘)))
22	11, 21, 7	cif 4487	. . 3 class if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0)
23	2, 3, 4, 5, 22	cmpo 7412	. 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))
24	1, 23	wceq 1570	1 wff C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))

This definition is referenced by:  bcval  14336