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 e. ( 0 ... N ) -> ( N _C K ) e. NN )

Proof

Step	Hyp	Ref	Expression
1		elfz3nn0	|- ( K e. ( 0 ... N ) -> N e. NN0 )
2		elfzelz	|- ( K e. ( 0 ... N ) -> K e. ZZ )
3		bccl	|- ( ( N e. NN0 /\ K e. ZZ ) -> ( N _C K ) e. NN0 )
4	1 2 3	syl2anc	|- ( K e. ( 0 ... N ) -> ( N _C K ) e. NN0 )
5		bcrpcl	|- ( K e. ( 0 ... N ) -> ( N _C K ) e. RR+ )
6	5	rpgt0d	|- ( K e. ( 0 ... N ) -> 0 < ( N _C K ) )
7		elnnnn0b	|- ( ( N _C K ) e. NN <-> ( ( N _C K ) e. NN0 /\ 0 < ( N _C K ) ) )
8	4 6 7	sylanbrc	|- ( K e. ( 0 ... N ) -> ( N _C K ) e. NN )