Definition df-bc 14256

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

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 14255	. 2 class C
2		vn	. . 3 setvar 𝑛
3		vk	. . 3 setvar 𝑘
4		cn0 12428	. . 3 class ℕ0
5		cz 12515	. . 3 class ℤ
6	3	cv 1546	. . . . 5 class 𝑘
7		cc0 11029	. . . . . 6 class 0
8	2	cv 1546	. . . . . 6 class 𝑛
9		cfz 13452	. . . . . 6 class ...
10	7, 8, 9	co 7356	. . . . 5 class (0...𝑛)
11	6, 10	wcel 2119	. . . 4 wff 𝑘 ∈ (0...𝑛)
12		cfa 14226	. . . . . 6 class !
13	8, 12	cfv 6485	. . . . 5 class (!‘𝑛)
14		cmin 11368	. . . . . . . 8 class −
15	8, 6, 14	co 7356	. . . . . . 7 class (𝑛 − 𝑘)
16	15, 12	cfv 6485	. . . . . 6 class (!‘(𝑛 − 𝑘))
17	6, 12	cfv 6485	. . . . . 6 class (!‘𝑘)
18		cmul 11034	. . . . . 6 class ·
19	16, 17, 18	co 7356	. . . . 5 class ((!‘(𝑛 − 𝑘)) · (!‘𝑘))
20		cdiv 11798	. . . . 5 class /
21	13, 19, 20	co 7356	. . . 4 class ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘)))
22	11, 21, 7	cif 4454	. . 3 class if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0)
23	2, 3, 4, 5, 22	cmpo 7358	. 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))
24	1, 23	wceq 1547	1 wff C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))

This definition is referenced by:  bcval  14257