Definition df-bc 14238

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

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 14237	. 2 class C
2		vn	. . 3 setvar 𝑛
3		vk	. . 3 setvar 𝑘
4		cn0 12413	. . 3 class ℕ0
5		cz 12500	. . 3 class ℤ
6	3	cv 1541	. . . . 5 class 𝑘
7		cc0 11038	. . . . . 6 class 0
8	2	cv 1541	. . . . . 6 class 𝑛
9		cfz 13435	. . . . . 6 class ...
10	7, 8, 9	co 7368	. . . . 5 class (0...𝑛)
11	6, 10	wcel 2114	. . . 4 wff 𝑘 ∈ (0...𝑛)
12		cfa 14208	. . . . . 6 class !
13	8, 12	cfv 6500	. . . . 5 class (!‘𝑛)
14		cmin 11376	. . . . . . . 8 class −
15	8, 6, 14	co 7368	. . . . . . 7 class (𝑛 − 𝑘)
16	15, 12	cfv 6500	. . . . . 6 class (!‘(𝑛 − 𝑘))
17	6, 12	cfv 6500	. . . . . 6 class (!‘𝑘)
18		cmul 11043	. . . . . 6 class ·
19	16, 17, 18	co 7368	. . . . 5 class ((!‘(𝑛 − 𝑘)) · (!‘𝑘))
20		cdiv 11806	. . . . 5 class /
21	13, 19, 20	co 7368	. . . 4 class ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘)))
22	11, 21, 7	cif 4481	. . 3 class if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0)
23	2, 3, 4, 5, 22	cmpo 7370	. 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))
24	1, 23	wceq 1542	1 wff C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))

This definition is referenced by:  bcval  14239