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	|- ( ph -> N e. NN0 )
	bccld.k	|- ( ph -> K e. ZZ )
Assertion	bccld	|- ( ph -> ( N _C K ) e. NN0 )

Proof

Step	Hyp	Ref	Expression
1		bccld.n	|- ( ph -> N e. NN0 )
2		bccld.k	|- ( ph -> K e. ZZ )
3		bccl	|- ( ( N e. NN0 /\ K e. ZZ ) -> ( N _C K ) e. NN0 )
4	1 2 3	syl2anc	|- ( ph -> ( N _C K ) e. NN0 )