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

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 13381 . 2 class C
2 vn . . 3 setvar 𝑛
3 vk . . 3 setvar 𝑘
4 cn0 11617 . . 3 class 0
5 cz 11703 . . 3 class
63cv 1657 . . . . 5 class 𝑘
7 cc0 10251 . . . . . 6 class 0
82cv 1657 . . . . . 6 class 𝑛
9 cfz 12618 . . . . . 6 class ...
107, 8, 9co 6904 . . . . 5 class (0...𝑛)
116, 10wcel 2166 . . . 4 wff 𝑘 ∈ (0...𝑛)
12 cfa 13352 . . . . . 6 class !
138, 12cfv 6122 . . . . 5 class (!‘𝑛)
14 cmin 10584 . . . . . . . 8 class
158, 6, 14co 6904 . . . . . . 7 class (𝑛𝑘)
1615, 12cfv 6122 . . . . . 6 class (!‘(𝑛𝑘))
176, 12cfv 6122 . . . . . 6 class (!‘𝑘)
18 cmul 10256 . . . . . 6 class ·
1916, 17, 18co 6904 . . . . 5 class ((!‘(𝑛𝑘)) · (!‘𝑘))
20 cdiv 11008 . . . . 5 class /
2113, 19, 20co 6904 . . . 4 class ((!‘𝑛) / ((!‘(𝑛𝑘)) · (!‘𝑘)))
2211, 21, 7cif 4305 . . 3 class if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛𝑘)) · (!‘𝑘))), 0)
232, 3, 4, 5, 22cmpt2 6906 . 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛𝑘)) · (!‘𝑘))), 0))
241, 23wceq 1658 1 wff C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛𝑘)) · (!‘𝑘))), 0))
Colors of variables: wff setvar class
This definition is referenced by:  bcval  13383
  Copyright terms: Public domain W3C validator