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

Proof

Step	Hyp	Ref	Expression
1		bcval2	|- ( K e. ( 0 ... N ) -> ( N _C K ) = ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) )
2		elfz3nn0	|- ( K e. ( 0 ... N ) -> N e. NN0 )
3	2	faccld	|- ( K e. ( 0 ... N ) -> ( ! ` N ) e. NN )
4		fznn0sub	|- ( K e. ( 0 ... N ) -> ( N - K ) e. NN0 )
5		elfznn0	|- ( K e. ( 0 ... N ) -> K e. NN0 )
6		faccl	|- ( ( N - K ) e. NN0 -> ( ! ` ( N - K ) ) e. NN )
7		faccl	|- ( K e. NN0 -> ( ! ` K ) e. NN )
8		nnmulcl	|- ( ( ( ! ` ( N - K ) ) e. NN /\ ( ! ` K ) e. NN ) -> ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) e. NN )
9	6 7 8	syl2an	|- ( ( ( N - K ) e. NN0 /\ K e. NN0 ) -> ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) e. NN )
10	4 5 9	syl2anc	|- ( K e. ( 0 ... N ) -> ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) e. NN )
11		nnrp	|- ( ( ! ` N ) e. NN -> ( ! ` N ) e. RR+ )
12		nnrp	|- ( ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) e. NN -> ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) e. RR+ )
13		rpdivcl	|- ( ( ( ! ` N ) e. RR+ /\ ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) e. RR+ ) -> ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) e. RR+ )
14	11 12 13	syl2an	|- ( ( ( ! ` N ) e. NN /\ ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) e. NN ) -> ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) e. RR+ )
15	3 10 14	syl2anc	|- ( K e. ( 0 ... N ) -> ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) e. RR+ )
16	1 15	eqeltrd	|- ( K e. ( 0 ... N ) -> ( N _C K ) e. RR+ )