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

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

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 10461 . 2  class  _C
2 vn . . 3  setvar  n
3 vk . . 3  setvar  k
4 cn0 8945 . . 3  class  NN0
5 cz 9022 . . 3  class  ZZ
63cv 1315 . . . . 5  class  k
7 cc0 7588 . . . . . 6  class  0
82cv 1315 . . . . . 6  class  n
9 cfz 9758 . . . . . 6  class  ...
107, 8, 9co 5742 . . . . 5  class  ( 0 ... n )
116, 10wcel 1465 . . . 4  wff  k  e.  ( 0 ... n
)
12 cfa 10439 . . . . . 6  class  !
138, 12cfv 5093 . . . . 5  class  ( ! `
 n )
14 cmin 7901 . . . . . . . 8  class  -
158, 6, 14co 5742 . . . . . . 7  class  ( n  -  k )
1615, 12cfv 5093 . . . . . 6  class  ( ! `
 ( n  -  k ) )
176, 12cfv 5093 . . . . . 6  class  ( ! `
 k )
18 cmul 7593 . . . . . 6  class  x.
1916, 17, 18co 5742 . . . . 5  class  ( ( ! `  ( n  -  k ) )  x.  ( ! `  k ) )
20 cdiv 8400 . . . . 5  class  /
2113, 19, 20co 5742 . . . 4  class  ( ( ! `  n )  /  ( ( ! `
 ( n  -  k ) )  x.  ( ! `  k
) ) )
2211, 21, 7cif 3444 . . 3  class  if ( k  e.  ( 0 ... n ) ,  ( ( ! `  n )  /  (
( ! `  (
n  -  k ) )  x.  ( ! `
 k ) ) ) ,  0 )
232, 3, 4, 5, 22cmpo 5744 . 2  class  ( n  e.  NN0 ,  k  e.  ZZ  |->  if ( k  e.  ( 0 ... n ) ,  ( ( ! `  n )  /  (
( ! `  (
n  -  k ) )  x.  ( ! `
 k ) ) ) ,  0 ) )
241, 23wceq 1316 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  10463
  Copyright terms: Public domain W3C validator