Metamath Proof Explorer


Theorem bccl2d

Description: Closure of the binomial coefficient, a deduction version. (Contributed by metakunt, 12-May-2024)

Ref Expression
Hypotheses bccl2d.1 ( 𝜑𝑁 ∈ ℕ )
bccl2d.2 ( 𝜑𝐾 ∈ ℕ0 )
bccl2d.3 ( 𝜑𝐾𝑁 )
Assertion bccl2d ( 𝜑 → ( 𝑁 C 𝐾 ) ∈ ℕ )

Proof

Step Hyp Ref Expression
1 bccl2d.1 ( 𝜑𝑁 ∈ ℕ )
2 bccl2d.2 ( 𝜑𝐾 ∈ ℕ0 )
3 bccl2d.3 ( 𝜑𝐾𝑁 )
4 2 nn0zd ( 𝜑𝐾 ∈ ℤ )
5 2 nn0ge0d ( 𝜑 → 0 ≤ 𝐾 )
6 4 5 3 3jca ( 𝜑 → ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾𝐾𝑁 ) )
7 1 nnzd ( 𝜑𝑁 ∈ ℤ )
8 0z 0 ∈ ℤ
9 elfz1 ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ( 0 ... 𝑁 ) ↔ ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾𝐾𝑁 ) ) )
10 8 9 mpan ( 𝑁 ∈ ℤ → ( 𝐾 ∈ ( 0 ... 𝑁 ) ↔ ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾𝐾𝑁 ) ) )
11 7 10 syl ( 𝜑 → ( 𝐾 ∈ ( 0 ... 𝑁 ) ↔ ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾𝐾𝑁 ) ) )
12 6 11 mpbird ( 𝜑𝐾 ∈ ( 0 ... 𝑁 ) )
13 bccl2 ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝐾 ) ∈ ℕ )
14 12 13 syl ( 𝜑 → ( 𝑁 C 𝐾 ) ∈ ℕ )