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 13664
Description: Define the binomial coefficient operation. For example, (5C3) = 10 (ex-bc 28233).

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 13663 . 2 class C
2 vn . . 3 setvar 𝑛
3 vk . . 3 setvar 𝑘
4 cn0 11890 . . 3 class 0
5 cz 11974 . . 3 class
63cv 1537 . . . . 5 class 𝑘
7 cc0 10529 . . . . . 6 class 0
82cv 1537 . . . . . 6 class 𝑛
9 cfz 12890 . . . . . 6 class ...
107, 8, 9co 7145 . . . . 5 class (0...𝑛)
116, 10wcel 2115 . . . 4 wff 𝑘 ∈ (0...𝑛)
12 cfa 13634 . . . . . 6 class !
138, 12cfv 6343 . . . . 5 class (!‘𝑛)
14 cmin 10862 . . . . . . . 8 class
158, 6, 14co 7145 . . . . . . 7 class (𝑛𝑘)
1615, 12cfv 6343 . . . . . 6 class (!‘(𝑛𝑘))
176, 12cfv 6343 . . . . . 6 class (!‘𝑘)
18 cmul 10534 . . . . . 6 class ·
1916, 17, 18co 7145 . . . . 5 class ((!‘(𝑛𝑘)) · (!‘𝑘))
20 cdiv 11289 . . . . 5 class /
2113, 19, 20co 7145 . . . 4 class ((!‘𝑛) / ((!‘(𝑛𝑘)) · (!‘𝑘)))
2211, 21, 7cif 4449 . . 3 class if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛𝑘)) · (!‘𝑘))), 0)
232, 3, 4, 5, 22cmpo 7147 . 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛𝑘)) · (!‘𝑘))), 0))
241, 23wceq 1538 1 wff C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛𝑘)) · (!‘𝑘))), 0))
Colors of variables: wff setvar class
This definition is referenced by:  bcval  13665
  Copyright terms: Public domain W3C validator