Theorem bccl2d

Description: Closure of the binomial coefficient, a deduction version. (Contributed by metakunt, 12-May-2024)

	Ref	Expression
Hypotheses	bccl2d.1	|- ( ph -> N e. NN )
	bccl2d.2	|- ( ph -> K e. NN0 )
	bccl2d.3	|- ( ph -> K <_ N )
Assertion	bccl2d	|- ( ph -> ( N _C K ) e. NN )

Proof

Step	Hyp	Ref	Expression
1		bccl2d.1	|- ( ph -> N e. NN )
2		bccl2d.2	|- ( ph -> K e. NN0 )
3		bccl2d.3	|- ( ph -> K <_ N )
4	2	nn0zd	|- ( ph -> K e. ZZ )
5	2	nn0ge0d	|- ( ph -> 0 <_ K )
6	4 5 3	3jca	|- ( ph -> ( K e. ZZ /\ 0 <_ K /\ K <_ N ) )
7	1	nnzd	|- ( ph -> N e. ZZ )
8		0z	|- 0 e. ZZ
9		elfz1	|- ( ( 0 e. ZZ /\ N e. ZZ ) -> ( K e. ( 0 ... N ) <-> ( K e. ZZ /\ 0 <_ K /\ K <_ N ) ) )
10	8 9	mpan	|- ( N e. ZZ -> ( K e. ( 0 ... N ) <-> ( K e. ZZ /\ 0 <_ K /\ K <_ N ) ) )
11	7 10	syl	|- ( ph -> ( K e. ( 0 ... N ) <-> ( K e. ZZ /\ 0 <_ K /\ K <_ N ) ) )
12	6 11	mpbird	|- ( ph -> K e. ( 0 ... N ) )
13		bccl2	|- ( K e. ( 0 ... N ) -> ( N _C K ) e. NN )
14	12 13	syl	|- ( ph -> ( N _C K ) e. NN )