This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 (0 \dots N) \to (\binom{N}{K}) \in ℝ^{+}$

Proof

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