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 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+ )