Definition df-bcc

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	$$⊢C_{𝑐}=\left(c\in ℂ,k\in {\mathbb{N}}_0⟼\frac{c^{\underset{\_}{k}}}{k!}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cbcc	$$class{C}_{𝑐}$$
1		vc	$$setvarc$$
2		cc	$$classℂ$$
3		vk	$$setvark$$
4		cn0	$$class{\mathbb{N}}_0$$
5	1	cv	$$setvarc$$
6		cfallfac	$$classFallFac$$
7	3	cv	$$setvark$$
8	5 7 6	co	$$class\left(c^{\underset{\_}{k}}\right)$$
9		cdiv	$$class÷$$
10		cfa	$$class!$$
11	7 10	cfv	$$classk!$$
12	8 11 9	co	$$class\left(\frac{c^{\underset{\_}{k}}}{k!}\right)$$
13	1 3 2 4 12	cmpo	$$class\left(c\in ℂ,k\in {\mathbb{N}}_0⟼\frac{c^{\underset{\_}{k}}}{k!}\right)$$
14	0 13	wceq	$$wff{C}_{𝑐}=\left(c\in ℂ,k\in {\mathbb{N}}_0⟼\frac{c^{\underset{\_}{k}}}{k!}\right)$$