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 𝐾 ) ∈ ℕ )