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 28159).
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 13652 | . 2 class C | |
2 | vn | . . 3 setvar 𝑛 | |
3 | vk | . . 3 setvar 𝑘 | |
4 | cn0 11886 | . . 3 class ℕ0 | |
5 | cz 11970 | . . 3 class ℤ | |
6 | 3 | cv 1527 | . . . . 5 class 𝑘 |
7 | cc0 10526 | . . . . . 6 class 0 | |
8 | 2 | cv 1527 | . . . . . 6 class 𝑛 |
9 | cfz 12882 | . . . . . 6 class ... | |
10 | 7, 8, 9 | co 7145 | . . . . 5 class (0...𝑛) |
11 | 6, 10 | wcel 2105 | . . . 4 wff 𝑘 ∈ (0...𝑛) |
12 | cfa 13623 | . . . . . 6 class ! | |
13 | 8, 12 | cfv 6349 | . . . . 5 class (!‘𝑛) |
14 | cmin 10859 | . . . . . . . 8 class − | |
15 | 8, 6, 14 | co 7145 | . . . . . . 7 class (𝑛 − 𝑘) |
16 | 15, 12 | cfv 6349 | . . . . . 6 class (!‘(𝑛 − 𝑘)) |
17 | 6, 12 | cfv 6349 | . . . . . 6 class (!‘𝑘) |
18 | cmul 10531 | . . . . . 6 class · | |
19 | 16, 17, 18 | co 7145 | . . . . 5 class ((!‘(𝑛 − 𝑘)) · (!‘𝑘)) |
20 | cdiv 11286 | . . . . 5 class / | |
21 | 13, 19, 20 | co 7145 | . . . 4 class ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))) |
22 | 11, 21, 7 | cif 4465 | . . 3 class if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0) |
23 | 2, 3, 4, 5, 22 | cmpo 7147 | . 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0)) |
24 | 1, 23 | wceq 1528 | 1 wff C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0)) |
Colors of variables: wff setvar class |
This definition is referenced by: bcval 13654 |
Copyright terms: Public domain | W3C validator |