Definition df-bcc 38536

Description: Define a generalized binomial coefficient operation, which unlike df-bc 13090 allows complex numbers for the first argument. (Contributed by Steve Rodriguez, 22-Apr-2020.)

Assertion

Ref	Expression
df-bcc	|- C𝑐 = ( c e. CC , k e. NN0 |-> ( ( c FallFac k ) / ( ! ` k ) ) )

Distinct variable group:   k, c

Detailed syntax breakdown of Definition df-bcc

Step	Hyp	Ref	Expression
1		cbcc 38535	. 2 class C𝑐
2		vc	. . 3 setvar c
3		vk	. . 3 setvar k
4		cc 9934	. . 3 class CC
5		cn0 11292	. . 3 class NN0
6	2	cv 1482	. . . . 5 class c
7	3	cv 1482	. . . . 5 class k
8		cfallfac 14735	. . . . 5 class FallFac
9	6, 7, 8	co 6650	. . . 4 class ( c FallFac k )
10		cfa 13060	. . . . 5 class !
11	7, 10	cfv 5888	. . . 4 class ( ! ` k )
12		cdiv 10684	. . . 4 class /
13	9, 11, 12	co 6650	. . 3 class ( ( c FallFac k ) / ( ! ` k ) )
14	2, 3, 4, 5, 13	cmpt2 6652	. 2 class ( c e. CC , k e. NN0 |-> ( ( c FallFac k ) / ( ! ` k ) ) )
15	1, 14	wceq 1483	1 wff C𝑐 = ( c e. CC , k e. NN0 |-> ( ( c FallFac k ) / ( ! ` k ) ) )

This definition is referenced by:  bccval  38537