Definition df-bc 14447

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

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 14446	. 2 class C
2		vn	. . 3 setvar 𝑛
3		vk	. . 3 setvar 𝑘
4		cn0 12606	. . 3 class ℕ0
5		cz 12693	. . 3 class ℤ
6	3	cv 1569	. . . . 5 class 𝑘
7		cc0 11200	. . . . . 6 class 0
8	2	cv 1569	. . . . . 6 class 𝑛
9		cfz 13639	. . . . . 6 class ...
10	7, 8, 9	co 7420	. . . . 5 class (0...𝑛)
11	6, 10	wcel 2145	. . . 4 wff 𝑘 ∈ (0...𝑛)
12		cfa 14417	. . . . . 6 class !
13	8, 12	cfv 6538	. . . . 5 class (!‘𝑛)
14		cmin 11541	. . . . . . . 8 class −
15	8, 6, 14	co 7420	. . . . . . 7 class (𝑛 − 𝑘)
16	15, 12	cfv 6538	. . . . . 6 class (!‘(𝑛 − 𝑘))
17	6, 12	cfv 6538	. . . . . 6 class (!‘𝑘)
18		cmul 11205	. . . . . 6 class ·
19	16, 17, 18	co 7420	. . . . 5 class ((!‘(𝑛 − 𝑘)) · (!‘𝑘))
20		cdiv 11973	. . . . 5 class /
21	13, 19, 20	co 7420	. . . 4 class ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘)))
22	11, 21, 7	cif 4482	. . 3 class if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0)
23	2, 3, 4, 5, 22	cmpo 7422	. 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))
24	1, 23	wceq 1570	1 wff C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))

This definition is used by:  bcval  14448