Theorem bcccl

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

	Ref	Expression
Hypotheses	bccval.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
	bccval.k	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
Assertion	bcccl	⊢ ( 𝜑 → ( 𝐶 C𝑐 𝐾 ) ∈ ℂ )

Proof

Step	Hyp	Ref	Expression
1		bccval.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
2		bccval.k	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
3	1 2	bccval	⊢ ( 𝜑 → ( 𝐶 C𝑐 𝐾 ) = ( ( 𝐶 FallFac 𝐾 ) / ( ! ‘ 𝐾 ) ) )
4		fallfaccl	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( 𝐶 FallFac 𝐾 ) ∈ ℂ )
5	1 2 4	syl2anc	⊢ ( 𝜑 → ( 𝐶 FallFac 𝐾 ) ∈ ℂ )
6		faccl	⊢ ( 𝐾 ∈ ℕ0 → ( ! ‘ 𝐾 ) ∈ ℕ )
7	2 6	syl	⊢ ( 𝜑 → ( ! ‘ 𝐾 ) ∈ ℕ )
8	7	nncnd	⊢ ( 𝜑 → ( ! ‘ 𝐾 ) ∈ ℂ )
9	7	nnne0d	⊢ ( 𝜑 → ( ! ‘ 𝐾 ) ≠ 0 )
10	5 8 9	divcld	⊢ ( 𝜑 → ( ( 𝐶 FallFac 𝐾 ) / ( ! ‘ 𝐾 ) ) ∈ ℂ )
11	3 10	eqeltrd	⊢ ( 𝜑 → ( 𝐶 C𝑐 𝐾 ) ∈ ℂ )