Description: Define a generalized binomial coefficient operation, which unlike df-bc allows complex numbers for the first argument. (Contributed by Steve Rodriguez, 22-Apr-2020)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-bcc | |- _Cc = ( c e. CC , k e. NN0 |-> ( ( c FallFac k ) / ( ! ` k ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cbcc | |- _Cc |
|
| 1 | vc | |- c |
|
| 2 | cc | |- CC |
|
| 3 | vk | |- k |
|
| 4 | cn0 | |- NN0 |
|
| 5 | 1 | cv | |- c |
| 6 | cfallfac | |- FallFac |
|
| 7 | 3 | cv | |- k |
| 8 | 5 7 6 | co | |- ( c FallFac k ) |
| 9 | cdiv | |- / |
|
| 10 | cfa | |- ! |
|
| 11 | 7 10 | cfv | |- ( ! ` k ) |
| 12 | 8 11 9 | co | |- ( ( c FallFac k ) / ( ! ` k ) ) |
| 13 | 1 3 2 4 12 | cmpo | |- ( c e. CC , k e. NN0 |-> ( ( c FallFac k ) / ( ! ` k ) ) ) |
| 14 | 0 13 | wceq | |- _Cc = ( c e. CC , k e. NN0 |-> ( ( c FallFac k ) / ( ! ` k ) ) ) |