Theorem bccld

Description: A binomial coefficient, in its extended domain, is a nonnegative integer. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	bccld.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	bccld.k	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
Assertion	bccld	⊢ ( 𝜑 → ( 𝑁 C 𝐾 ) ∈ ℕ0 )

Proof

Step	Hyp	Ref	Expression
1		bccld.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2		bccld.k	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
3		bccl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) → ( 𝑁 C 𝐾 ) ∈ ℕ0 )
4	1 2 3	syl2anc	⊢ ( 𝜑 → ( 𝑁 C 𝐾 ) ∈ ℕ0 )