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

Metamath Proof Explorer

Theorem elfz2nn0

Description: Membership in a finite set of sequential nonnegative integers. (Contributed by NM, 16-Sep-2005) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion elfz2nn0 ⊢ K ∈ 0 … N ↔ K ∈ ℕ 0 ∧ N ∈ ℕ 0 ∧ K ≤ N

Proof

Step Hyp Ref Expression
1 elnn0uz ⊢ K ∈ ℕ 0 ↔ K ∈ ℤ ≥ 0
2 1 anbi1i ⊢ K ∈ ℕ 0 ∧ N ∈ ℤ ≥ K ↔ K ∈ ℤ ≥ 0 ∧ N ∈ ℤ ≥ K
3 eluznn0 ⊢ K ∈ ℕ 0 ∧ N ∈ ℤ ≥ K → N ∈ ℕ 0
4 eluzle ⊢ N ∈ ℤ ≥ K → K ≤ N
5 4 adantl ⊢ K ∈ ℕ 0 ∧ N ∈ ℤ ≥ K → K ≤ N
6 3 5 jca ⊢ K ∈ ℕ 0 ∧ N ∈ ℤ ≥ K → N ∈ ℕ 0 ∧ K ≤ N
7 nn0z ⊢ K ∈ ℕ 0 → K ∈ ℤ
8 nn0z ⊢ N ∈ ℕ 0 → N ∈ ℤ
9 eluz ⊢ K ∈ ℤ ∧ N ∈ ℤ → N ∈ ℤ ≥ K ↔ K ≤ N
10 7 8 9 syl2an ⊢ K ∈ ℕ 0 ∧ N ∈ ℕ 0 → N ∈ ℤ ≥ K ↔ K ≤ N
11 10 biimprd ⊢ K ∈ ℕ 0 ∧ N ∈ ℕ 0 → K ≤ N → N ∈ ℤ ≥ K
12 11 impr ⊢ K ∈ ℕ 0 ∧ N ∈ ℕ 0 ∧ K ≤ N → N ∈ ℤ ≥ K
13 6 12 impbida ⊢ K ∈ ℕ 0 → N ∈ ℤ ≥ K ↔ N ∈ ℕ 0 ∧ K ≤ N
14 13 pm5.32i ⊢ K ∈ ℕ 0 ∧ N ∈ ℤ ≥ K ↔ K ∈ ℕ 0 ∧ N ∈ ℕ 0 ∧ K ≤ N
15 2 14 bitr3i ⊢ K ∈ ℤ ≥ 0 ∧ N ∈ ℤ ≥ K ↔ K ∈ ℕ 0 ∧ N ∈ ℕ 0 ∧ K ≤ N
16 elfzuzb ⊢ K ∈ 0 … N ↔ K ∈ ℤ ≥ 0 ∧ N ∈ ℤ ≥ K
17 3anass ⊢ K ∈ ℕ 0 ∧ N ∈ ℕ 0 ∧ K ≤ N ↔ K ∈ ℕ 0 ∧ N ∈ ℕ 0 ∧ K ≤ N
18 15 16 17 3bitr4i ⊢ K ∈ 0 … N ↔ K ∈ ℕ 0 ∧ N ∈ ℕ 0 ∧ K ≤ N