Definition df-bc 13659

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

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 13658	. 2 class C
2		vn	. . 3 setvar 𝑛
3		vk	. . 3 setvar 𝑘
4		cn0 11885	. . 3 class ℕ0
5		cz 11969	. . 3 class ℤ
6	3	cv 1537	. . . . 5 class 𝑘
7		cc0 10526	. . . . . 6 class 0
8	2	cv 1537	. . . . . 6 class 𝑛
9		cfz 12885	. . . . . 6 class ...
10	7, 8, 9	co 7135	. . . . 5 class (0...𝑛)
11	6, 10	wcel 2111	. . . 4 wff 𝑘 ∈ (0...𝑛)
12		cfa 13629	. . . . . 6 class !
13	8, 12	cfv 6324	. . . . 5 class (!‘𝑛)
14		cmin 10859	. . . . . . . 8 class −
15	8, 6, 14	co 7135	. . . . . . 7 class (𝑛 − 𝑘)
16	15, 12	cfv 6324	. . . . . 6 class (!‘(𝑛 − 𝑘))
17	6, 12	cfv 6324	. . . . . 6 class (!‘𝑘)
18		cmul 10531	. . . . . 6 class ·
19	16, 17, 18	co 7135	. . . . 5 class ((!‘(𝑛 − 𝑘)) · (!‘𝑘))
20		cdiv 11286	. . . . 5 class /
21	13, 19, 20	co 7135	. . . 4 class ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘)))
22	11, 21, 7	cif 4425	. . 3 class if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0)
23	2, 3, 4, 5, 22	cmpo 7137	. 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))
24	1, 23	wceq 1538	1 wff C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))

This definition is referenced by:  bcval  13660