Definition df-bc 14026

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

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 14025	. 2 class C
2		vn	. . 3 setvar 𝑛
3		vk	. . 3 setvar 𝑘
4		cn0 12242	. . 3 class ℕ0
5		cz 12328	. . 3 class ℤ
6	3	cv 1538	. . . . 5 class 𝑘
7		cc0 10880	. . . . . 6 class 0
8	2	cv 1538	. . . . . 6 class 𝑛
9		cfz 13248	. . . . . 6 class ...
10	7, 8, 9	co 7284	. . . . 5 class (0...𝑛)
11	6, 10	wcel 2107	. . . 4 wff 𝑘 ∈ (0...𝑛)
12		cfa 13996	. . . . . 6 class !
13	8, 12	cfv 6437	. . . . 5 class (!‘𝑛)
14		cmin 11214	. . . . . . . 8 class −
15	8, 6, 14	co 7284	. . . . . . 7 class (𝑛 − 𝑘)
16	15, 12	cfv 6437	. . . . . 6 class (!‘(𝑛 − 𝑘))
17	6, 12	cfv 6437	. . . . . 6 class (!‘𝑘)
18		cmul 10885	. . . . . 6 class ·
19	16, 17, 18	co 7284	. . . . 5 class ((!‘(𝑛 − 𝑘)) · (!‘𝑘))
20		cdiv 11641	. . . . 5 class /
21	13, 19, 20	co 7284	. . . 4 class ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘)))
22	11, 21, 7	cif 4460	. . 3 class if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0)
23	2, 3, 4, 5, 22	cmpo 7286	. 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))
24	1, 23	wceq 1539	1 wff C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))

This definition is referenced by:  bcval  14027