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𝑐 = ( 𝑐 ∈ ℂ , 𝑘 ∈ ℕ0 ↦ ( ( 𝑐 FallFac 𝑘 ) / ( ! ‘ 𝑘 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cbcc	⊢ C𝑐
1		vc	⊢ 𝑐
2		cc	⊢ ℂ
3		vk	⊢ 𝑘
4		cn0	⊢ ℕ0
5	1	cv	⊢ 𝑐
6		cfallfac	⊢ FallFac
7	3	cv	⊢ 𝑘
8	5 7 6	co	⊢ ( 𝑐 FallFac 𝑘 )
9		cdiv	⊢ /
10		cfa	⊢ !
11	7 10	cfv	⊢ ( ! ‘ 𝑘 )
12	8 11 9	co	⊢ ( ( 𝑐 FallFac 𝑘 ) / ( ! ‘ 𝑘 ) )
13	1 3 2 4 12	cmpo	⊢ ( 𝑐 ∈ ℂ , 𝑘 ∈ ℕ0 ↦ ( ( 𝑐 FallFac 𝑘 ) / ( ! ‘ 𝑘 ) ) )
14	0 13	wceq	⊢ C𝑐 = ( 𝑐 ∈ ℂ , 𝑘 ∈ ℕ0 ↦ ( ( 𝑐 FallFac 𝑘 ) / ( ! ‘ 𝑘 ) ) )