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 28540).
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 13873 | . 2 class C | |
2 | vn | . . 3 setvar 𝑛 | |
3 | vk | . . 3 setvar 𝑘 | |
4 | cn0 12095 | . . 3 class ℕ0 | |
5 | cz 12181 | . . 3 class ℤ | |
6 | 3 | cv 1542 | . . . . 5 class 𝑘 |
7 | cc0 10734 | . . . . . 6 class 0 | |
8 | 2 | cv 1542 | . . . . . 6 class 𝑛 |
9 | cfz 13100 | . . . . . 6 class ... | |
10 | 7, 8, 9 | co 7218 | . . . . 5 class (0...𝑛) |
11 | 6, 10 | wcel 2110 | . . . 4 wff 𝑘 ∈ (0...𝑛) |
12 | cfa 13844 | . . . . . 6 class ! | |
13 | 8, 12 | cfv 6385 | . . . . 5 class (!‘𝑛) |
14 | cmin 11067 | . . . . . . . 8 class − | |
15 | 8, 6, 14 | co 7218 | . . . . . . 7 class (𝑛 − 𝑘) |
16 | 15, 12 | cfv 6385 | . . . . . 6 class (!‘(𝑛 − 𝑘)) |
17 | 6, 12 | cfv 6385 | . . . . . 6 class (!‘𝑘) |
18 | cmul 10739 | . . . . . 6 class · | |
19 | 16, 17, 18 | co 7218 | . . . . 5 class ((!‘(𝑛 − 𝑘)) · (!‘𝑘)) |
20 | cdiv 11494 | . . . . 5 class / | |
21 | 13, 19, 20 | co 7218 | . . . 4 class ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))) |
22 | 11, 21, 7 | cif 4444 | . . 3 class if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0) |
23 | 2, 3, 4, 5, 22 | cmpo 7220 | . 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0)) |
24 | 1, 23 | wceq 1543 | 1 wff C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0)) |
Colors of variables: wff setvar class |
This definition is referenced by: bcval 13875 |
Copyright terms: Public domain | W3C validator |