Theorem bccl2d

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

	Ref	Expression
Hypotheses	bccl2d.1	$$⊢\phi \to N\in \mathbb{N}$$
	bccl2d.2	$$⊢\phi \to K\in {\mathbb{N}}_0$$
	bccl2d.3	$$⊢\phi \to K\le N$$
Assertion	bccl2d	$$⊢\phi \to \left(\genfrac{}{}{0ex}{}{N}{K}\right)\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		bccl2d.1	$$⊢\phi \to N\in \mathbb{N}$$
2		bccl2d.2	$$⊢\phi \to K\in {\mathbb{N}}_0$$
3		bccl2d.3	$$⊢\phi \to K\le N$$
4	2	nn0zd	$$⊢\phi \to K\in \mathbb{Z}$$
5	2	nn0ge0d	$$⊢\phi \to 0\le K$$
6	4 5 3	3jca	$$⊢\phi \to \left(K\in \mathbb{Z}\wedge 0\le K\wedge K\le N\right)$$
7	1	nnzd	$$⊢\phi \to N\in \mathbb{Z}$$
8		0z	$$⊢0\in \mathbb{Z}$$
9		elfz1	$$⊢\left(0\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(K\in \left(0\dots N\right)\leftrightarrow \left(K\in \mathbb{Z}\wedge 0\le K\wedge K\le N\right)\right)$$
10	8 9	mpan	$$⊢N\in \mathbb{Z}\to \left(K\in \left(0\dots N\right)\leftrightarrow \left(K\in \mathbb{Z}\wedge 0\le K\wedge K\le N\right)\right)$$
11	7 10	syl	$$⊢\phi \to \left(K\in \left(0\dots N\right)\leftrightarrow \left(K\in \mathbb{Z}\wedge 0\le K\wedge K\le N\right)\right)$$
12	6 11	mpbird	$$⊢\phi \to K\in \left(0\dots N\right)$$
13		bccl2	$$⊢K\in \left(0\dots N\right)\to \left(\genfrac{}{}{0ex}{}{N}{K}\right)\in \mathbb{N}$$
14	12 13	syl	$$⊢\phi \to \left(\genfrac{}{}{0ex}{}{N}{K}\right)\in \mathbb{N}$$