Definition df-bc 14316

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

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 14315	. 2 class C
2		vn	. . 3 setvar 𝑛
3		vk	. . 3 setvar 𝑘
4		cn0 12481	. . 3 class ℕ0
5		cz 12568	. . 3 class ℤ
6	3	cv 1559	. . . . 5 class 𝑘
7		cc0 11073	. . . . . 6 class 0
8	2	cv 1559	. . . . . 6 class 𝑛
9		cfz 13512	. . . . . 6 class ...
10	7, 8, 9	co 7396	. . . . 5 class (0...𝑛)
11	6, 10	wcel 2142	. . . 4 wff 𝑘 ∈ (0...𝑛)
12		cfa 14286	. . . . . 6 class !
13	8, 12	cfv 6521	. . . . 5 class (!‘𝑛)
14		cmin 11414	. . . . . . . 8 class −
15	8, 6, 14	co 7396	. . . . . . 7 class (𝑛 − 𝑘)
16	15, 12	cfv 6521	. . . . . 6 class (!‘(𝑛 − 𝑘))
17	6, 12	cfv 6521	. . . . . 6 class (!‘𝑘)
18		cmul 11078	. . . . . 6 class ·
19	16, 17, 18	co 7396	. . . . 5 class ((!‘(𝑛 − 𝑘)) · (!‘𝑘))
20		cdiv 11844	. . . . 5 class /
21	13, 19, 20	co 7396	. . . 4 class ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘)))
22	11, 21, 7	cif 4480	. . 3 class if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0)
23	2, 3, 4, 5, 22	cmpo 7398	. 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))
24	1, 23	wceq 1560	1 wff C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))

This definition is referenced by:  bcval  14317