MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-bc Structured version   Visualization version   GIF version

Definition df-bc 14280
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.)

Assertion
Ref Expression
df-bc C = (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛𝑘)) · (!‘𝑘))), 0))
Distinct variable group:   𝑘,𝑛

Detailed syntax breakdown of Definition df-bc
StepHypRef 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
63cv 1533 . . . . 5 class 𝑘
7 cc0 11124 . . . . . 6 class 0
82cv 1533 . . . . . 6 class 𝑛
9 cfz 13502 . . . . . 6 class ...
107, 8, 9co 7414 . . . . 5 class (0...𝑛)
116, 10wcel 2099 . . . 4 wff 𝑘 ∈ (0...𝑛)
12 cfa 14250 . . . . . 6 class !
138, 12cfv 6542 . . . . 5 class (!‘𝑛)
14 cmin 11460 . . . . . . . 8 class
158, 6, 14co 7414 . . . . . . 7 class (𝑛𝑘)
1615, 12cfv 6542 . . . . . 6 class (!‘(𝑛𝑘))
176, 12cfv 6542 . . . . . 6 class (!‘𝑘)
18 cmul 11129 . . . . . 6 class ·
1916, 17, 18co 7414 . . . . 5 class ((!‘(𝑛𝑘)) · (!‘𝑘))
20 cdiv 11887 . . . . 5 class /
2113, 19, 20co 7414 . . . 4 class ((!‘𝑛) / ((!‘(𝑛𝑘)) · (!‘𝑘)))
2211, 21, 7cif 4524 . . 3 class if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛𝑘)) · (!‘𝑘))), 0)
232, 3, 4, 5, 22cmpo 7416 . 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛𝑘)) · (!‘𝑘))), 0))
241, 23wceq 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