Theorem bcrpcl

Description: Closure of the binomial coefficient in the positive reals. (This is mostly a lemma before we have bccl2 .) (Contributed by Mario Carneiro, 10-Mar-2014)

	Ref	Expression
Assertion	bcrpcl	$$⊢K\in \left(0\dots N\right)\to \left(\genfrac{}{}{0ex}{}{N}{K}\right)\in {ℝ}^{+}$$

Proof

Step	Hyp	Ref	Expression
1		bcval2	$$⊢K\in \left(0\dots N\right)\to \left(\genfrac{}{}{0ex}{}{N}{K}\right)=\frac{N!}{\left(N-K\right)!K!}$$
2		elfz3nn0	$$⊢K\in \left(0\dots N\right)\to N\in {\mathbb{N}}_0$$
3	2	faccld	$$⊢K\in \left(0\dots N\right)\to N!\in \mathbb{N}$$
4		fznn0sub	$$⊢K\in \left(0\dots N\right)\to N-K\in {\mathbb{N}}_0$$
5		elfznn0	$$⊢K\in \left(0\dots N\right)\to K\in {\mathbb{N}}_0$$
6		faccl	$$⊢N-K\in {\mathbb{N}}_0\to \left(N-K\right)!\in \mathbb{N}$$
7		faccl	$$⊢K\in {\mathbb{N}}_0\to K!\in \mathbb{N}$$
8		nnmulcl	$$⊢\left(\left(N-K\right)!\in \mathbb{N}\wedge K!\in \mathbb{N}\right)\to \left(N-K\right)!K!\in \mathbb{N}$$
9	6 7 8	syl2an	$$⊢\left(N-K\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\to \left(N-K\right)!K!\in \mathbb{N}$$
10	4 5 9	syl2anc	$$⊢K\in \left(0\dots N\right)\to \left(N-K\right)!K!\in \mathbb{N}$$
11		nnrp	$$⊢N!\in \mathbb{N}\to N!\in {ℝ}^{+}$$
12		nnrp	$$⊢\left(N-K\right)!K!\in \mathbb{N}\to \left(N-K\right)!K!\in {ℝ}^{+}$$
13		rpdivcl	$$⊢\left(N!\in {ℝ}^{+}\wedge \left(N-K\right)!K!\in {ℝ}^{+}\right)\to \frac{N!}{\left(N-K\right)!K!}\in {ℝ}^{+}$$
14	11 12 13	syl2an	$$⊢\left(N!\in \mathbb{N}\wedge \left(N-K\right)!K!\in \mathbb{N}\right)\to \frac{N!}{\left(N-K\right)!K!}\in {ℝ}^{+}$$
15	3 10 14	syl2anc	$$⊢K\in \left(0\dots N\right)\to \frac{N!}{\left(N-K\right)!K!}\in {ℝ}^{+}$$
16	1 15	eqeltrd	$$⊢K\in \left(0\dots N\right)\to \left(\genfrac{}{}{0ex}{}{N}{K}\right)\in {ℝ}^{+}$$