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 ( 𝐾 ∈ ( 0 ... 𝑁 ) ↔ ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁 ) )

Proof

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