Definition df-bc 10661

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

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". (𝑁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 10660	. 2 class C
2		vn	. . 3 setvar 𝑛
3		vk	. . 3 setvar 𝑘
4		cn0 9114	. . 3 class ℕ0
5		cz 9191	. . 3 class ℤ
6	3	cv 1342	. . . . 5 class 𝑘
7		cc0 7753	. . . . . 6 class 0
8	2	cv 1342	. . . . . 6 class 𝑛
9		cfz 9944	. . . . . 6 class ...
10	7, 8, 9	co 5842	. . . . 5 class (0...𝑛)
11	6, 10	wcel 2136	. . . 4 wff 𝑘 ∈ (0...𝑛)
12		cfa 10638	. . . . . 6 class !
13	8, 12	cfv 5188	. . . . 5 class (!‘𝑛)
14		cmin 8069	. . . . . . . 8 class −
15	8, 6, 14	co 5842	. . . . . . 7 class (𝑛 − 𝑘)
16	15, 12	cfv 5188	. . . . . 6 class (!‘(𝑛 − 𝑘))
17	6, 12	cfv 5188	. . . . . 6 class (!‘𝑘)
18		cmul 7758	. . . . . 6 class ·
19	16, 17, 18	co 5842	. . . . 5 class ((!‘(𝑛 − 𝑘)) · (!‘𝑘))
20		cdiv 8568	. . . . 5 class /
21	13, 19, 20	co 5842	. . . 4 class ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘)))
22	11, 21, 7	cif 3520	. . 3 class if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0)
23	2, 3, 4, 5, 22	cmpo 5844	. 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))
24	1, 23	wceq 1343	1 wff C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))

This definition is referenced by:  bcval  10662