Definition df-bc 14338

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

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 14337	. 2 class C
2		vn	. . 3 setvar 𝑛
3		vk	. . 3 setvar 𝑘
4		cn0 12503	. . 3 class ℕ0
5		cz 12590	. . 3 class ℤ
6	3	cv 1566	. . . . 5 class 𝑘
7		cc0 11099	. . . . . 6 class 0
8	2	cv 1566	. . . . . 6 class 𝑛
9		cfz 13534	. . . . . 6 class ...
10	7, 8, 9	co 7411	. . . . 5 class (0...𝑛)
11	6, 10	wcel 2149	. . . 4 wff 𝑘 ∈ (0...𝑛)
12		cfa 14308	. . . . . 6 class !
13	8, 12	cfv 6537	. . . . 5 class (!‘𝑛)
14		cmin 11440	. . . . . . . 8 class −
15	8, 6, 14	co 7411	. . . . . . 7 class (𝑛 − 𝑘)
16	15, 12	cfv 6537	. . . . . 6 class (!‘(𝑛 − 𝑘))
17	6, 12	cfv 6537	. . . . . 6 class (!‘𝑘)
18		cmul 11104	. . . . . 6 class ·
19	16, 17, 18	co 7411	. . . . 5 class ((!‘(𝑛 − 𝑘)) · (!‘𝑘))
20		cdiv 11870	. . . . 5 class /
21	13, 19, 20	co 7411	. . . 4 class ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘)))
22	11, 21, 7	cif 4492	. . 3 class if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0)
23	2, 3, 4, 5, 22	cmpo 7413	. 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))
24	1, 23	wceq 1567	1 wff C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))

This definition is referenced by:  bcval  14339