# 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 ${⊢}{N}\in {ℕ}_{0}\to \left({K}\in \left(0\dots {N}\right)↔\left({K}\in {ℕ}_{0}\wedge {K}\le {N}\right)\right)$

### Proof

Step Hyp Ref Expression
1 0z ${⊢}0\in ℤ$
2 nn0z ${⊢}{N}\in {ℕ}_{0}\to {N}\in ℤ$
3 elfz1 ${⊢}\left(0\in ℤ\wedge {N}\in ℤ\right)\to \left({K}\in \left(0\dots {N}\right)↔\left({K}\in ℤ\wedge 0\le {K}\wedge {K}\le {N}\right)\right)$
4 1 2 3 sylancr ${⊢}{N}\in {ℕ}_{0}\to \left({K}\in \left(0\dots {N}\right)↔\left({K}\in ℤ\wedge 0\le {K}\wedge {K}\le {N}\right)\right)$
5 df-3an ${⊢}\left({K}\in ℤ\wedge 0\le {K}\wedge {K}\le {N}\right)↔\left(\left({K}\in ℤ\wedge 0\le {K}\right)\wedge {K}\le {N}\right)$
6 elnn0z ${⊢}{K}\in {ℕ}_{0}↔\left({K}\in ℤ\wedge 0\le {K}\right)$
7 6 anbi1i ${⊢}\left({K}\in {ℕ}_{0}\wedge {K}\le {N}\right)↔\left(\left({K}\in ℤ\wedge 0\le {K}\right)\wedge {K}\le {N}\right)$
8 5 7 bitr4i ${⊢}\left({K}\in ℤ\wedge 0\le {K}\wedge {K}\le {N}\right)↔\left({K}\in {ℕ}_{0}\wedge {K}\le {N}\right)$
9 4 8 syl6bb ${⊢}{N}\in {ℕ}_{0}\to \left({K}\in \left(0\dots {N}\right)↔\left({K}\in {ℕ}_{0}\wedge {K}\le {N}\right)\right)$