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