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

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 14341 . 2 class C
2 vn . . 3 setvar 𝑛
3 vk . . 3 setvar 𝑘
4 cn0 12526 . . 3 class 0
5 cz 12613 . . 3 class
63cv 1539 . . . . 5 class 𝑘
7 cc0 11155 . . . . . 6 class 0
82cv 1539 . . . . . 6 class 𝑛
9 cfz 13547 . . . . . 6 class ...
107, 8, 9co 7431 . . . . 5 class (0...𝑛)
116, 10wcel 2108 . . . 4 wff 𝑘 ∈ (0...𝑛)
12 cfa 14312 . . . . . 6 class !
138, 12cfv 6561 . . . . 5 class (!‘𝑛)
14 cmin 11492 . . . . . . . 8 class
158, 6, 14co 7431 . . . . . . 7 class (𝑛𝑘)
1615, 12cfv 6561 . . . . . 6 class (!‘(𝑛𝑘))
176, 12cfv 6561 . . . . . 6 class (!‘𝑘)
18 cmul 11160 . . . . . 6 class ·
1916, 17, 18co 7431 . . . . 5 class ((!‘(𝑛𝑘)) · (!‘𝑘))
20 cdiv 11920 . . . . 5 class /
2113, 19, 20co 7431 . . . 4 class ((!‘𝑛) / ((!‘(𝑛𝑘)) · (!‘𝑘)))
2211, 21, 7cif 4525 . . 3 class if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛𝑘)) · (!‘𝑘))), 0)
232, 3, 4, 5, 22cmpo 7433 . 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛𝑘)) · (!‘𝑘))), 0))
241, 23wceq 1540 1 wff C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛𝑘)) · (!‘𝑘))), 0))
Colors of variables: wff setvar class
This definition is referenced by:  bcval  14343
  Copyright terms: Public domain W3C validator