Definition df-bc 14352

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

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 14351	. 2 class C
2		vn	. . 3 setvar 𝑛
3		vk	. . 3 setvar 𝑘
4		cn0 12553	. . 3 class ℕ0
5		cz 12639	. . 3 class ℤ
6	3	cv 1536	. . . . 5 class 𝑘
7		cc0 11184	. . . . . 6 class 0
8	2	cv 1536	. . . . . 6 class 𝑛
9		cfz 13567	. . . . . 6 class ...
10	7, 8, 9	co 7448	. . . . 5 class (0...𝑛)
11	6, 10	wcel 2108	. . . 4 wff 𝑘 ∈ (0...𝑛)
12		cfa 14322	. . . . . 6 class !
13	8, 12	cfv 6573	. . . . 5 class (!‘𝑛)
14		cmin 11520	. . . . . . . 8 class −
15	8, 6, 14	co 7448	. . . . . . 7 class (𝑛 − 𝑘)
16	15, 12	cfv 6573	. . . . . 6 class (!‘(𝑛 − 𝑘))
17	6, 12	cfv 6573	. . . . . 6 class (!‘𝑘)
18		cmul 11189	. . . . . 6 class ·
19	16, 17, 18	co 7448	. . . . 5 class ((!‘(𝑛 − 𝑘)) · (!‘𝑘))
20		cdiv 11947	. . . . 5 class /
21	13, 19, 20	co 7448	. . . 4 class ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘)))
22	11, 21, 7	cif 4548	. . 3 class if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0)
23	2, 3, 4, 5, 22	cmpo 7450	. 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))
24	1, 23	wceq 1537	1 wff C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))

This definition is referenced by:  bcval  14353