![]() |
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 30236).
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 14279 | . 2 class C | |
2 | vn | . . 3 setvar 𝑛 | |
3 | vk | . . 3 setvar 𝑘 | |
4 | cn0 12488 | . . 3 class ℕ0 | |
5 | cz 12574 | . . 3 class ℤ | |
6 | 3 | cv 1533 | . . . . 5 class 𝑘 |
7 | cc0 11124 | . . . . . 6 class 0 | |
8 | 2 | cv 1533 | . . . . . 6 class 𝑛 |
9 | cfz 13502 | . . . . . 6 class ... | |
10 | 7, 8, 9 | co 7414 | . . . . 5 class (0...𝑛) |
11 | 6, 10 | wcel 2099 | . . . 4 wff 𝑘 ∈ (0...𝑛) |
12 | cfa 14250 | . . . . . 6 class ! | |
13 | 8, 12 | cfv 6542 | . . . . 5 class (!‘𝑛) |
14 | cmin 11460 | . . . . . . . 8 class − | |
15 | 8, 6, 14 | co 7414 | . . . . . . 7 class (𝑛 − 𝑘) |
16 | 15, 12 | cfv 6542 | . . . . . 6 class (!‘(𝑛 − 𝑘)) |
17 | 6, 12 | cfv 6542 | . . . . . 6 class (!‘𝑘) |
18 | cmul 11129 | . . . . . 6 class · | |
19 | 16, 17, 18 | co 7414 | . . . . 5 class ((!‘(𝑛 − 𝑘)) · (!‘𝑘)) |
20 | cdiv 11887 | . . . . 5 class / | |
21 | 13, 19, 20 | co 7414 | . . . 4 class ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))) |
22 | 11, 21, 7 | cif 4524 | . . 3 class if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0) |
23 | 2, 3, 4, 5, 22 | cmpo 7416 | . 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0)) |
24 | 1, 23 | wceq 1534 | 1 wff C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛 − 𝑘)) · (!‘𝑘))), 0)) |
Colors of variables: wff setvar class |
This definition is referenced by: bcval 14281 |
Copyright terms: Public domain | W3C validator |