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