Definition df-bc 10727

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

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". (𝑁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 10726	. 2 class C
2		vn	. . 3 setvar 𝑛
3		vk	. . 3 setvar 𝑘
4		cn0 9175	. . 3 class ℕ0
5		cz 9252	. . 3 class ℤ
6	3	cv 1352	. . . . 5 class 𝑘
7		cc0 7810	. . . . . 6 class 0
8	2	cv 1352	. . . . . 6 class 𝑛
9		cfz 10007	. . . . . 6 class ...
10	7, 8, 9	co 5874	. . . . 5 class (0...𝑛)
11	6, 10	wcel 2148	. . . 4 wff 𝑘 ∈ (0...𝑛)
12		cfa 10704	. . . . . 6 class !
13	8, 12	cfv 5216	. . . . 5 class (!‘𝑛)
14		cmin 8127	. . . . . . . 8 class −
15	8, 6, 14	co 5874	. . . . . . 7 class (𝑛 − 𝑘)
16	15, 12	cfv 5216	. . . . . 6 class (!‘(𝑛 − 𝑘))
17	6, 12	cfv 5216	. . . . . 6 class (!‘𝑘)
18		cmul 7815	. . . . . 6 class ·
19	16, 17, 18	co 5874	. . . . 5 class ((!‘(𝑛 − 𝑘)) · (!‘𝑘))
20		cdiv 8628	. . . . 5 class /
21	13, 19, 20	co 5874	. . . 4 class ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘)))
22	11, 21, 7	cif 3534	. . 3 class if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0)
23	2, 3, 4, 5, 22	cmpo 5876	. 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))
24	1, 23	wceq 1353	1 wff C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))

This definition is referenced by:  bcval  10728