Metamath Proof Explorer


Definition df-bc

Description: Define the binomial coefficient operation. For example, ( 5C 3 ) = 1 0 ( ex-bc ).

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 ( 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)

Ref Expression
Assertion df-bc
|- _C = ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cbc
 |-  _C
1 vn
 |-  n
2 cn0
 |-  NN0
3 vk
 |-  k
4 cz
 |-  ZZ
5 3 cv
 |-  k
6 cc0
 |-  0
7 cfz
 |-  ...
8 1 cv
 |-  n
9 6 8 7 co
 |-  ( 0 ... n )
10 5 9 wcel
 |-  k e. ( 0 ... n )
11 cfa
 |-  !
12 8 11 cfv
 |-  ( ! ` n )
13 cdiv
 |-  /
14 cmin
 |-  -
15 8 5 14 co
 |-  ( n - k )
16 15 11 cfv
 |-  ( ! ` ( n - k ) )
17 cmul
 |-  x.
18 5 11 cfv
 |-  ( ! ` k )
19 16 18 17 co
 |-  ( ( ! ` ( n - k ) ) x. ( ! ` k ) )
20 12 19 13 co
 |-  ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) )
21 10 20 6 cif
 |-  if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 )
22 1 3 2 4 21 cmpo
 |-  ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) )
23 0 22 wceq
 |-  _C = ( n e. NN0 , k e. ZZ |-> if ( k e. ( 0 ... n ) , ( ( ! ` n ) / ( ( ! ` ( n - k ) ) x. ( ! ` k ) ) ) , 0 ) )