Metamath Proof Explorer


Theorem fznn0

Description: Characterization of a finite set of sequential nonnegative integers. (Contributed by NM, 1-Aug-2005)

Ref Expression
Assertion fznn0 ( 𝑁 ∈ ℕ0 → ( 𝐾 ∈ ( 0 ... 𝑁 ) ↔ ( 𝐾 ∈ ℕ0𝐾𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 0z 0 ∈ ℤ
2 nn0z ( 𝑁 ∈ ℕ0𝑁 ∈ ℤ )
3 elfz1 ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ( 0 ... 𝑁 ) ↔ ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾𝐾𝑁 ) ) )
4 1 2 3 sylancr ( 𝑁 ∈ ℕ0 → ( 𝐾 ∈ ( 0 ... 𝑁 ) ↔ ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾𝐾𝑁 ) ) )
5 df-3an ( ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾𝐾𝑁 ) ↔ ( ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾 ) ∧ 𝐾𝑁 ) )
6 elnn0z ( 𝐾 ∈ ℕ0 ↔ ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾 ) )
7 6 anbi1i ( ( 𝐾 ∈ ℕ0𝐾𝑁 ) ↔ ( ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾 ) ∧ 𝐾𝑁 ) )
8 5 7 bitr4i ( ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾𝐾𝑁 ) ↔ ( 𝐾 ∈ ℕ0𝐾𝑁 ) )
9 4 8 bitrdi ( 𝑁 ∈ ℕ0 → ( 𝐾 ∈ ( 0 ... 𝑁 ) ↔ ( 𝐾 ∈ ℕ0𝐾𝑁 ) ) )