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

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 ∧ 𝐾 ≤ 𝑁 ) ) )