Definition df-bc 13945

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

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 13944	. 2 class C
2		vn	. . 3 setvar 𝑛
3		vk	. . 3 setvar 𝑘
4		cn0 12163	. . 3 class ℕ0
5		cz 12249	. . 3 class ℤ
6	3	cv 1538	. . . . 5 class 𝑘
7		cc0 10802	. . . . . 6 class 0
8	2	cv 1538	. . . . . 6 class 𝑛
9		cfz 13168	. . . . . 6 class ...
10	7, 8, 9	co 7255	. . . . 5 class (0...𝑛)
11	6, 10	wcel 2108	. . . 4 wff 𝑘 ∈ (0...𝑛)
12		cfa 13915	. . . . . 6 class !
13	8, 12	cfv 6418	. . . . 5 class (!‘𝑛)
14		cmin 11135	. . . . . . . 8 class −
15	8, 6, 14	co 7255	. . . . . . 7 class (𝑛 − 𝑘)
16	15, 12	cfv 6418	. . . . . 6 class (!‘(𝑛 − 𝑘))
17	6, 12	cfv 6418	. . . . . 6 class (!‘𝑘)
18		cmul 10807	. . . . . 6 class ·
19	16, 17, 18	co 7255	. . . . 5 class ((!‘(𝑛 − 𝑘)) · (!‘𝑘))
20		cdiv 11562	. . . . 5 class /
21	13, 19, 20	co 7255	. . . 4 class ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘)))
22	11, 21, 7	cif 4456	. . 3 class if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0)
23	2, 3, 4, 5, 22	cmpo 7257	. 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))
24	1, 23	wceq 1539	1 wff C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))

This definition is referenced by:  bcval  13946