Definition df-bc 14460

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

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 14459	. 2 class C
2		vn	. . 3 setvar 𝑛
3		vk	. . 3 setvar 𝑘
4		cn0 12619	. . 3 class ℕ0
5		cz 12706	. . 3 class ℤ
6	3	cv 1568	. . . . 5 class 𝑘
7		cc0 11213	. . . . . 6 class 0
8	2	cv 1568	. . . . . 6 class 𝑛
9		cfz 13652	. . . . . 6 class ...
10	7, 8, 9	co 7430	. . . . 5 class (0...𝑛)
11	6, 10	wcel 2146	. . . 4 wff 𝑘 ∈ (0...𝑛)
12		cfa 14430	. . . . . 6 class !
13	8, 12	cfv 6547	. . . . 5 class (!‘𝑛)
14		cmin 11554	. . . . . . . 8 class −
15	8, 6, 14	co 7430	. . . . . . 7 class (𝑛 − 𝑘)
16	15, 12	cfv 6547	. . . . . 6 class (!‘(𝑛 − 𝑘))
17	6, 12	cfv 6547	. . . . . 6 class (!‘𝑘)
18		cmul 11218	. . . . . 6 class ·
19	16, 17, 18	co 7430	. . . . 5 class ((!‘(𝑛 − 𝑘)) · (!‘𝑘))
20		cdiv 11986	. . . . 5 class /
21	13, 19, 20	co 7430	. . . 4 class ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘)))
22	11, 21, 7	cif 4485	. . 3 class if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0)
23	2, 3, 4, 5, 22	cmpo 7432	. 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))
24	1, 23	wceq 1569	1 wff C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))

This definition is used by:  bcval  14461