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

Proof

Step	Hyp	Ref	Expression
1		bcval2	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝐾 ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) )
2		elfz3nn0	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℕ0 )
3	2	faccld	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ! ‘ 𝑁 ) ∈ ℕ )
4		fznn0sub	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 − 𝐾 ) ∈ ℕ0 )
5		elfznn0	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ℕ0 )
6		faccl	⊢ ( ( 𝑁 − 𝐾 ) ∈ ℕ0 → ( ! ‘ ( 𝑁 − 𝐾 ) ) ∈ ℕ )
7		faccl	⊢ ( 𝐾 ∈ ℕ0 → ( ! ‘ 𝐾 ) ∈ ℕ )
8		nnmulcl	⊢ ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) ∈ ℕ ∧ ( ! ‘ 𝐾 ) ∈ ℕ ) → ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ∈ ℕ )
9	6 7 8	syl2an	⊢ ( ( ( 𝑁 − 𝐾 ) ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ∈ ℕ )
10	4 5 9	syl2anc	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ∈ ℕ )
11		nnrp	⊢ ( ( ! ‘ 𝑁 ) ∈ ℕ → ( ! ‘ 𝑁 ) ∈ ℝ+ )
12		nnrp	⊢ ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ∈ ℕ → ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ∈ ℝ+ )
13		rpdivcl	⊢ ( ( ( ! ‘ 𝑁 ) ∈ ℝ+ ∧ ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ∈ ℝ+ ) → ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) ∈ ℝ+ )
14	11 12 13	syl2an	⊢ ( ( ( ! ‘ 𝑁 ) ∈ ℕ ∧ ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ∈ ℕ ) → ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) ∈ ℝ+ )
15	3 10 14	syl2anc	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) ∈ ℝ+ )
16	1 15	eqeltrd	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝐾 ) ∈ ℝ+ )