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

Definition df-bc 11316
Description: Define the binomial coefficient operation. 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".  ( N  _C  K ) is read " N choose  K." Definition of binomial coefficient in [Gleason] p. 295. As suggested by Gleason, we define it to be 0 when  0  <_  k  <_  n does not hold. (Contributed by NM, 10-Jul-2005.)
Assertion
Ref Expression
df-bc  |-  _C  =  ( n  e.  NN0 ,  k  e.  ZZ  |->  if ( k  e.  ( 0 ... n ) ,  ( ( ! `
 n )  / 
( ( ! `  ( n  -  k
) )  x.  ( ! `  k )
) ) ,  0 ) )
Distinct variable group:    k, n

Detailed syntax breakdown of Definition df-bc
StepHypRef Expression
1 cbc 11315 . 2  class  _C
2 vn . . 3  set  n
3 vk . . 3  set  k
4 cn0 9965 . . 3  class  NN0
5 cz 10024 . . 3  class  ZZ
63cv 1622 . . . . 5  class  k
7 cc0 8737 . . . . . 6  class  0
82cv 1622 . . . . . 6  class  n
9 cfz 10782 . . . . . 6  class  ...
107, 8, 9co 5858 . . . . 5  class  ( 0 ... n )
116, 10wcel 1684 . . . 4  wff  k  e.  ( 0 ... n
)
12 cfa 11288 . . . . . 6  class  !
138, 12cfv 5255 . . . . 5  class  ( ! `
 n )
14 cmin 9037 . . . . . . . 8  class  -
158, 6, 14co 5858 . . . . . . 7  class  ( n  -  k )
1615, 12cfv 5255 . . . . . 6  class  ( ! `
 ( n  -  k ) )
176, 12cfv 5255 . . . . . 6  class  ( ! `
 k )
18 cmul 8742 . . . . . 6  class  x.
1916, 17, 18co 5858 . . . . 5  class  ( ( ! `  ( n  -  k ) )  x.  ( ! `  k ) )
20 cdiv 9423 . . . . 5  class  /
2113, 19, 20co 5858 . . . 4  class  ( ( ! `  n )  /  ( ( ! `
 ( n  -  k ) )  x.  ( ! `  k
) ) )
2211, 21, 7cif 3565 . . 3  class  if ( k  e.  ( 0 ... n ) ,  ( ( ! `  n )  /  (
( ! `  (
n  -  k ) )  x.  ( ! `
 k ) ) ) ,  0 )
232, 3, 4, 5, 22cmpt2 5860 . 2  class  ( n  e.  NN0 ,  k  e.  ZZ  |->  if ( k  e.  ( 0 ... n ) ,  ( ( ! `  n )  /  (
( ! `  (
n  -  k ) )  x.  ( ! `
 k ) ) ) ,  0 ) )
241, 23wceq 1623 1  wff  _C  =  ( n  e.  NN0 ,  k  e.  ZZ  |->  if ( k  e.  ( 0 ... n ) ,  ( ( ! `
 n )  / 
( ( ! `  ( n  -  k
) )  x.  ( ! `  k )
) ) ,  0 ) )
Colors of variables: wff set class
This definition is referenced by:  bcval  11317
  Copyright terms: Public domain W3C validator