Definition df-bcc 41908

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

Assertion

Ref	Expression
df-bcc	⊢ C𝑐 = (𝑐 ∈ ℂ, 𝑘 ∈ ℕ0 ↦ ((𝑐 FallFac 𝑘) / (!‘𝑘)))

Distinct variable group:   𝑘,𝑐

Detailed syntax breakdown of Definition df-bcc

Step	Hyp	Ref	Expression
1		cbcc 41907	. 2 class C𝑐
2		vc	. . 3 setvar 𝑐
3		vk	. . 3 setvar 𝑘
4		cc 10853	. . 3 class ℂ
5		cn0 12216	. . 3 class ℕ0
6	2	cv 1540	. . . . 5 class 𝑐
7	3	cv 1540	. . . . 5 class 𝑘
8		cfallfac 15695	. . . . 5 class FallFac
9	6, 7, 8	co 7268	. . . 4 class (𝑐 FallFac 𝑘)
10		cfa 13968	. . . . 5 class !
11	7, 10	cfv 6430	. . . 4 class (!‘𝑘)
12		cdiv 11615	. . . 4 class /
13	9, 11, 12	co 7268	. . 3 class ((𝑐 FallFac 𝑘) / (!‘𝑘))
14	2, 3, 4, 5, 13	cmpo 7270	. 2 class (𝑐 ∈ ℂ, 𝑘 ∈ ℕ0 ↦ ((𝑐 FallFac 𝑘) / (!‘𝑘)))
15	1, 14	wceq 1541	1 wff C𝑐 = (𝑐 ∈ ℂ, 𝑘 ∈ ℕ0 ↦ ((𝑐 FallFac 𝑘) / (!‘𝑘)))

This definition is referenced by:  bccval  41909