MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-bc Structured version   Visualization version   GIF version

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

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
StepHypRef Expression
1 cbc 14337 . 2 class C
2 vn . . 3 setvar 𝑛
3 vk . . 3 setvar 𝑘
4 cn0 12523 . . 3 class 0
5 cz 12610 . . 3 class
63cv 1535 . . . . 5 class 𝑘
7 cc0 11152 . . . . . 6 class 0
82cv 1535 . . . . . 6 class 𝑛
9 cfz 13543 . . . . . 6 class ...
107, 8, 9co 7430 . . . . 5 class (0...𝑛)
116, 10wcel 2105 . . . 4 wff 𝑘 ∈ (0...𝑛)
12 cfa 14308 . . . . . 6 class !
138, 12cfv 6562 . . . . 5 class (!‘𝑛)
14 cmin 11489 . . . . . . . 8 class
158, 6, 14co 7430 . . . . . . 7 class (𝑛𝑘)
1615, 12cfv 6562 . . . . . 6 class (!‘(𝑛𝑘))
176, 12cfv 6562 . . . . . 6 class (!‘𝑘)
18 cmul 11157 . . . . . 6 class ·
1916, 17, 18co 7430 . . . . 5 class ((!‘(𝑛𝑘)) · (!‘𝑘))
20 cdiv 11917 . . . . 5 class /
2113, 19, 20co 7430 . . . 4 class ((!‘𝑛) / ((!‘(𝑛𝑘)) · (!‘𝑘)))
2211, 21, 7cif 4530 . . 3 class if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛𝑘)) · (!‘𝑘))), 0)
232, 3, 4, 5, 22cmpo 7432 . 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛𝑘)) · (!‘𝑘))), 0))
241, 23wceq 1536 1 wff C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛𝑘)) · (!‘𝑘))), 0))
Colors of variables: wff setvar class
This definition is referenced by:  bcval  14339
  Copyright terms: Public domain W3C validator