ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-bc Unicode version

Definition df-bc 10682
Description: Define the binomial coefficient operation. For example,  ( 5  _C  3 )  =  1 0 (ex-bc 13764).

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 10681 . 2  class  _C
2 vn . . 3  setvar  n
3 vk . . 3  setvar  k
4 cn0 9135 . . 3  class  NN0
5 cz 9212 . . 3  class  ZZ
63cv 1347 . . . . 5  class  k
7 cc0 7774 . . . . . 6  class  0
82cv 1347 . . . . . 6  class  n
9 cfz 9965 . . . . . 6  class  ...
107, 8, 9co 5853 . . . . 5  class  ( 0 ... n )
116, 10wcel 2141 . . . 4  wff  k  e.  ( 0 ... n
)
12 cfa 10659 . . . . . 6  class  !
138, 12cfv 5198 . . . . 5  class  ( ! `
 n )
14 cmin 8090 . . . . . . . 8  class  -
158, 6, 14co 5853 . . . . . . 7  class  ( n  -  k )
1615, 12cfv 5198 . . . . . 6  class  ( ! `
 ( n  -  k ) )
176, 12cfv 5198 . . . . . 6  class  ( ! `
 k )
18 cmul 7779 . . . . . 6  class  x.
1916, 17, 18co 5853 . . . . 5  class  ( ( ! `  ( n  -  k ) )  x.  ( ! `  k ) )
20 cdiv 8589 . . . . 5  class  /
2113, 19, 20co 5853 . . . 4  class  ( ( ! `  n )  /  ( ( ! `
 ( n  -  k ) )  x.  ( ! `  k
) ) )
2211, 21, 7cif 3526 . . 3  class  if ( k  e.  ( 0 ... n ) ,  ( ( ! `  n )  /  (
( ! `  (
n  -  k ) )  x.  ( ! `
 k ) ) ) ,  0 )
232, 3, 4, 5, 22cmpo 5855 . 2  class  ( n  e.  NN0 ,  k  e.  ZZ  |->  if ( k  e.  ( 0 ... n ) ,  ( ( ! `  n )  /  (
( ! `  (
n  -  k ) )  x.  ( ! `
 k ) ) ) ,  0 ) )
241, 23wceq 1348 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  10683
  Copyright terms: Public domain W3C validator