Metamath Proof Explorer

Theorem bccl2

Description: A binomial coefficient, in its standard domain, is a positive integer. (Contributed by NM, 3-Jan-2006) (Revised by Mario Carneiro, 10-Mar-2014)

		Ref	Expression
	Assertion	bccl2	$⊢ K \in (0 \dots N) \to (\binom{N}{K}) \in ℕ$

Proof

Step	Hyp	Ref	Expression
1		elfz3nn0	$⊢ K \in (0 \dots N) \to N \in ℕ_{0}$
2		elfzelz	$⊢ K \in (0 \dots N) \to K \in ℤ$
3		bccl	$⊢ (N \in ℕ_{0} \land K \in ℤ) \to (\binom{N}{K}) \in ℕ_{0}$
4	1 2 3	syl2anc	$⊢ K \in (0 \dots N) \to (\binom{N}{K}) \in ℕ_{0}$
5		bcrpcl	$⊢ K \in (0 \dots N) \to (\binom{N}{K}) \in ℝ^{+}$
6	5	rpgt0d	$⊢ K \in (0 \dots N) \to 0 < (\binom{N}{K})$
7		elnnnn0b	$⊢ (\binom{N}{K}) \in ℕ \leftrightarrow ((\binom{N}{K}) \in ℕ_{0} \land 0 < (\binom{N}{K}))$
8	4 6 7	sylanbrc	$⊢ K \in (0 \dots N) \to (\binom{N}{K}) \in ℕ$