Definition df-bc 14275

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

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 14274	. 2 class C
2		vn	. . 3 setvar 𝑛
3		vk	. . 3 setvar 𝑘
4		cn0 12449	. . 3 class ℕ0
5		cz 12536	. . 3 class ℤ
6	3	cv 1539	. . . . 5 class 𝑘
7		cc0 11075	. . . . . 6 class 0
8	2	cv 1539	. . . . . 6 class 𝑛
9		cfz 13475	. . . . . 6 class ...
10	7, 8, 9	co 7390	. . . . 5 class (0...𝑛)
11	6, 10	wcel 2109	. . . 4 wff 𝑘 ∈ (0...𝑛)
12		cfa 14245	. . . . . 6 class !
13	8, 12	cfv 6514	. . . . 5 class (!‘𝑛)
14		cmin 11412	. . . . . . . 8 class −
15	8, 6, 14	co 7390	. . . . . . 7 class (𝑛 − 𝑘)
16	15, 12	cfv 6514	. . . . . 6 class (!‘(𝑛 − 𝑘))
17	6, 12	cfv 6514	. . . . . 6 class (!‘𝑘)
18		cmul 11080	. . . . . 6 class ·
19	16, 17, 18	co 7390	. . . . 5 class ((!‘(𝑛 − 𝑘)) · (!‘𝑘))
20		cdiv 11842	. . . . 5 class /
21	13, 19, 20	co 7390	. . . 4 class ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘)))
22	11, 21, 7	cif 4491	. . 3 class if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0)
23	2, 3, 4, 5, 22	cmpo 7392	. 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))
24	1, 23	wceq 1540	1 wff C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))

This definition is referenced by:  bcval  14276