This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bccld

Description: A binomial coefficient, in its extended domain, is a nonnegative integer. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses bccld.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
bccld.k ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
Assertion bccld ( 𝜑 → ( 𝑁 C 𝐾 ) ∈ ℕ0 )

Proof

Step Hyp Ref Expression
1 bccld.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2 bccld.k ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
3 bccl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) → ( 𝑁 C 𝐾 ) ∈ ℕ0 )
4 1 2 3 syl2anc ⊢ ( 𝜑 → ( 𝑁 C 𝐾 ) ∈ ℕ0 )