![]() |
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 30480).
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 14337 | . 2 class C | |
2 | vn | . . 3 setvar 𝑛 | |
3 | vk | . . 3 setvar 𝑘 | |
4 | cn0 12523 | . . 3 class ℕ0 | |
5 | cz 12610 | . . 3 class ℤ | |
6 | 3 | cv 1535 | . . . . 5 class 𝑘 |
7 | cc0 11152 | . . . . . 6 class 0 | |
8 | 2 | cv 1535 | . . . . . 6 class 𝑛 |
9 | cfz 13543 | . . . . . 6 class ... | |
10 | 7, 8, 9 | co 7430 | . . . . 5 class (0...𝑛) |
11 | 6, 10 | wcel 2105 | . . . 4 wff 𝑘 ∈ (0...𝑛) |
12 | cfa 14308 | . . . . . 6 class ! | |
13 | 8, 12 | cfv 6562 | . . . . 5 class (!‘𝑛) |
14 | cmin 11489 | . . . . . . . 8 class − | |
15 | 8, 6, 14 | co 7430 | . . . . . . 7 class (𝑛 − 𝑘) |
16 | 15, 12 | cfv 6562 | . . . . . 6 class (!‘(𝑛 − 𝑘)) |
17 | 6, 12 | cfv 6562 | . . . . . 6 class (!‘𝑘) |
18 | cmul 11157 | . . . . . 6 class · | |
19 | 16, 17, 18 | co 7430 | . . . . 5 class ((!‘(𝑛 − 𝑘)) · (!‘𝑘)) |
20 | cdiv 11917 | . . . . 5 class / | |
21 | 13, 19, 20 | co 7430 | . . . 4 class ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))) |
22 | 11, 21, 7 | cif 4530 | . . 3 class if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0) |
23 | 2, 3, 4, 5, 22 | cmpo 7432 | . 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0)) |
24 | 1, 23 | wceq 1536 | 1 wff C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0)) |
Colors of variables: wff setvar class |
This definition is referenced by: bcval 14339 |
Copyright terms: Public domain | W3C validator |