| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-bc | Structured version Visualization version GIF version | ||
| 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.) |
| Ref | Expression |
|---|---|
| df-bc | ⊢ C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0)) |
| Step | Hyp | Ref | 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 ℤ | |
| 6 | 3 | cv 1539 | . . . . 5 class 𝑘 |
| 7 | cc0 11155 | . . . . . 6 class 0 | |
| 8 | 2 | cv 1539 | . . . . . 6 class 𝑛 |
| 9 | cfz 13547 | . . . . . 6 class ... | |
| 10 | 7, 8, 9 | co 7431 | . . . . 5 class (0...𝑛) |
| 11 | 6, 10 | wcel 2108 | . . . 4 wff 𝑘 ∈ (0...𝑛) |
| 12 | cfa 14312 | . . . . . 6 class ! | |
| 13 | 8, 12 | cfv 6561 | . . . . 5 class (!‘𝑛) |
| 14 | cmin 11492 | . . . . . . . 8 class − | |
| 15 | 8, 6, 14 | co 7431 | . . . . . . 7 class (𝑛 − 𝑘) |
| 16 | 15, 12 | cfv 6561 | . . . . . 6 class (!‘(𝑛 − 𝑘)) |
| 17 | 6, 12 | cfv 6561 | . . . . . 6 class (!‘𝑘) |
| 18 | cmul 11160 | . . . . . 6 class · | |
| 19 | 16, 17, 18 | co 7431 | . . . . 5 class ((!‘(𝑛 − 𝑘)) · (!‘𝑘)) |
| 20 | cdiv 11920 | . . . . 5 class / | |
| 21 | 13, 19, 20 | co 7431 | . . . 4 class ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))) |
| 22 | 11, 21, 7 | cif 4525 | . . 3 class if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0) |
| 23 | 2, 3, 4, 5, 22 | cmpo 7433 | . 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0)) |
| 24 | 1, 23 | wceq 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 |