Definition df-bc 14216

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

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 14215	. 2 class C
2		vn	. . 3 setvar 𝑛
3		vk	. . 3 setvar 𝑘
4		cn0 12387	. . 3 class ℕ0
5		cz 12474	. . 3 class ℤ
6	3	cv 1540	. . . . 5 class 𝑘
7		cc0 11012	. . . . . 6 class 0
8	2	cv 1540	. . . . . 6 class 𝑛
9		cfz 13413	. . . . . 6 class ...
10	7, 8, 9	co 7352	. . . . 5 class (0...𝑛)
11	6, 10	wcel 2111	. . . 4 wff 𝑘 ∈ (0...𝑛)
12		cfa 14186	. . . . . 6 class !
13	8, 12	cfv 6487	. . . . 5 class (!‘𝑛)
14		cmin 11350	. . . . . . . 8 class −
15	8, 6, 14	co 7352	. . . . . . 7 class (𝑛 − 𝑘)
16	15, 12	cfv 6487	. . . . . 6 class (!‘(𝑛 − 𝑘))
17	6, 12	cfv 6487	. . . . . 6 class (!‘𝑘)
18		cmul 11017	. . . . . 6 class ·
19	16, 17, 18	co 7352	. . . . 5 class ((!‘(𝑛 − 𝑘)) · (!‘𝑘))
20		cdiv 11780	. . . . 5 class /
21	13, 19, 20	co 7352	. . . 4 class ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘)))
22	11, 21, 7	cif 4474	. . 3 class if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0)
23	2, 3, 4, 5, 22	cmpo 7354	. 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))
24	1, 23	wceq 1541	1 wff C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))

This definition is referenced by:  bcval  14217