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 13874
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.)

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

Detailed syntax breakdown of Definition df-bc
StepHypRef 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
63cv 1542 . . . . 5 class 𝑘
7 cc0 10734 . . . . . 6 class 0
82cv 1542 . . . . . 6 class 𝑛
9 cfz 13100 . . . . . 6 class ...
107, 8, 9co 7218 . . . . 5 class (0...𝑛)
116, 10wcel 2110 . . . 4 wff 𝑘 ∈ (0...𝑛)
12 cfa 13844 . . . . . 6 class !
138, 12cfv 6385 . . . . 5 class (!‘𝑛)
14 cmin 11067 . . . . . . . 8 class
158, 6, 14co 7218 . . . . . . 7 class (𝑛𝑘)
1615, 12cfv 6385 . . . . . 6 class (!‘(𝑛𝑘))
176, 12cfv 6385 . . . . . 6 class (!‘𝑘)
18 cmul 10739 . . . . . 6 class ·
1916, 17, 18co 7218 . . . . 5 class ((!‘(𝑛𝑘)) · (!‘𝑘))
20 cdiv 11494 . . . . 5 class /
2113, 19, 20co 7218 . . . 4 class ((!‘𝑛) / ((!‘(𝑛𝑘)) · (!‘𝑘)))
2211, 21, 7cif 4444 . . 3 class if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛𝑘)) · (!‘𝑘))), 0)
232, 3, 4, 5, 22cmpo 7220 . 2 class (𝑛 ∈ ℕ0, 𝑘 ∈ ℤ ↦ if(𝑘 ∈ (0...𝑛), ((!‘𝑛) / ((!‘(𝑛𝑘)) · (!‘𝑘))), 0))
241, 23wceq 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