![]() |
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 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.) |
Ref | Expression |
---|---|
df-bc | ⊢ C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0)) |
Step | Hyp | Ref | 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 ℤ | |
6 | 3 | cv 1657 | . . . . 5 class 𝑘 |
7 | cc0 10251 | . . . . . 6 class 0 | |
8 | 2 | cv 1657 | . . . . . 6 class 𝑛 |
9 | cfz 12618 | . . . . . 6 class ... | |
10 | 7, 8, 9 | co 6904 | . . . . 5 class (0...𝑛) |
11 | 6, 10 | wcel 2166 | . . . 4 wff 𝑘 ∈ (0...𝑛) |
12 | cfa 13352 | . . . . . 6 class ! | |
13 | 8, 12 | cfv 6122 | . . . . 5 class (!‘𝑛) |
14 | cmin 10584 | . . . . . . . 8 class − | |
15 | 8, 6, 14 | co 6904 | . . . . . . 7 class (𝑛 − 𝑘) |
16 | 15, 12 | cfv 6122 | . . . . . 6 class (!‘(𝑛 − 𝑘)) |
17 | 6, 12 | cfv 6122 | . . . . . 6 class (!‘𝑘) |
18 | cmul 10256 | . . . . . 6 class · | |
19 | 16, 17, 18 | co 6904 | . . . . 5 class ((!‘(𝑛 − 𝑘)) · (!‘𝑘)) |
20 | cdiv 11008 | . . . . 5 class / | |
21 | 13, 19, 20 | co 6904 | . . . 4 class ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))) |
22 | 11, 21, 7 | cif 4305 | . . 3 class if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0) |
23 | 2, 3, 4, 5, 22 | cmpt2 6906 | . 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0)) |
24 | 1, 23 | wceq 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 |