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	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝐾 ) ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		elfz3nn0	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℕ0 )
2		elfzelz	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ℤ )
3		bccl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) → ( 𝑁 C 𝐾 ) ∈ ℕ0 )
4	1 2 3	syl2anc	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝐾 ) ∈ ℕ0 )
5		bcrpcl	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝐾 ) ∈ ℝ+ )
6	5	rpgt0d	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 0 < ( 𝑁 C 𝐾 ) )
7		elnnnn0b	⊢ ( ( 𝑁 C 𝐾 ) ∈ ℕ ↔ ( ( 𝑁 C 𝐾 ) ∈ ℕ0 ∧ 0 < ( 𝑁 C 𝐾 ) ) )
8	4 6 7	sylanbrc	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝐾 ) ∈ ℕ )