Definition df-bc 14289

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

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 14288	. 2 class C
2		vn	. . 3 setvar 𝑛
3		vk	. . 3 setvar 𝑘
4		cn0 12497	. . 3 class ℕ0
5		cz 12583	. . 3 class ℤ
6	3	cv 1533	. . . . 5 class 𝑘
7		cc0 11133	. . . . . 6 class 0
8	2	cv 1533	. . . . . 6 class 𝑛
9		cfz 13511	. . . . . 6 class ...
10	7, 8, 9	co 7415	. . . . 5 class (0...𝑛)
11	6, 10	wcel 2099	. . . 4 wff 𝑘 ∈ (0...𝑛)
12		cfa 14259	. . . . . 6 class !
13	8, 12	cfv 6543	. . . . 5 class (!‘𝑛)
14		cmin 11469	. . . . . . . 8 class −
15	8, 6, 14	co 7415	. . . . . . 7 class (𝑛 − 𝑘)
16	15, 12	cfv 6543	. . . . . 6 class (!‘(𝑛 − 𝑘))
17	6, 12	cfv 6543	. . . . . 6 class (!‘𝑘)
18		cmul 11138	. . . . . 6 class ·
19	16, 17, 18	co 7415	. . . . 5 class ((!‘(𝑛 − 𝑘)) · (!‘𝑘))
20		cdiv 11896	. . . . 5 class /
21	13, 19, 20	co 7415	. . . 4 class ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘)))
22	11, 21, 7	cif 4525	. . 3 class if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0)
23	2, 3, 4, 5, 22	cmpo 7417	. 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))
24	1, 23	wceq 1534	1 wff C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0))

This definition is referenced by:  bcval  14290

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »