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 28231).
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 13663 | . 2 class C | |
2 | vn | . . 3 setvar 𝑛 | |
3 | vk | . . 3 setvar 𝑘 | |
4 | cn0 11898 | . . 3 class ℕ0 | |
5 | cz 11982 | . . 3 class ℤ | |
6 | 3 | cv 1536 | . . . . 5 class 𝑘 |
7 | cc0 10537 | . . . . . 6 class 0 | |
8 | 2 | cv 1536 | . . . . . 6 class 𝑛 |
9 | cfz 12893 | . . . . . 6 class ... | |
10 | 7, 8, 9 | co 7156 | . . . . 5 class (0...𝑛) |
11 | 6, 10 | wcel 2114 | . . . 4 wff 𝑘 ∈ (0...𝑛) |
12 | cfa 13634 | . . . . . 6 class ! | |
13 | 8, 12 | cfv 6355 | . . . . 5 class (!‘𝑛) |
14 | cmin 10870 | . . . . . . . 8 class − | |
15 | 8, 6, 14 | co 7156 | . . . . . . 7 class (𝑛 − 𝑘) |
16 | 15, 12 | cfv 6355 | . . . . . 6 class (!‘(𝑛 − 𝑘)) |
17 | 6, 12 | cfv 6355 | . . . . . 6 class (!‘𝑘) |
18 | cmul 10542 | . . . . . 6 class · | |
19 | 16, 17, 18 | co 7156 | . . . . 5 class ((!‘(𝑛 − 𝑘)) · (!‘𝑘)) |
20 | cdiv 11297 | . . . . 5 class / | |
21 | 13, 19, 20 | co 7156 | . . . 4 class ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))) |
22 | 11, 21, 7 | cif 4467 | . . 3 class if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0) |
23 | 2, 3, 4, 5, 22 | cmpo 7158 | . 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0)) |
24 | 1, 23 | wceq 1537 | 1 wff C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0)) |
Colors of variables: wff setvar class |
This definition is referenced by: bcval 13665 |
Copyright terms: Public domain | W3C validator |