Theorem bcccl

Description: Closure of the generalized binomial coefficient. (Contributed by Steve Rodriguez, 22-Apr-2020)

	Ref	Expression
Hypotheses	bccval.c	$$⊢\phi \to C\in ℂ$$
	bccval.k	$$⊢\phi \to K\in {\mathbb{N}}_0$$
Assertion	bcccl	$$⊢\phi \to C{C}_{𝑐}K\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		bccval.c	$$⊢\phi \to C\in ℂ$$
2		bccval.k	$$⊢\phi \to K\in {\mathbb{N}}_0$$
3	1 2	bccval	$$⊢\phi \to C{C}_{𝑐}K=\frac{C^{\underset{\_}{K}}}{K!}$$
4		fallfaccl	$$⊢\left(C\in ℂ\wedge K\in {\mathbb{N}}_0\right)\to C^{\underset{\_}{K}}\in ℂ$$
5	1 2 4	syl2anc	$$⊢\phi \to C^{\underset{\_}{K}}\in ℂ$$
6		faccl	$$⊢K\in {\mathbb{N}}_0\to K!\in \mathbb{N}$$
7	2 6	syl	$$⊢\phi \to K!\in \mathbb{N}$$
8	7	nncnd	$$⊢\phi \to K!\in ℂ$$
9	7	nnne0d	$$⊢\phi \to K!\ne 0$$
10	5 8 9	divcld	$$⊢\phi \to \frac{C^{\underset{\_}{K}}}{K!}\in ℂ$$
11	3 10	eqeltrd	$$⊢\phi \to C{C}_{𝑐}K\in ℂ$$