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

Metamath Proof Explorer

Theorem elfz

Description: Membership in a finite set of sequential integers. (Contributed by NM, 29-Sep-2005)

Ref Expression
Assertion elfz ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 elfz1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) )
2 3anass ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ↔ ( 𝐾 ∈ ℤ ∧ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) )
3 2 baib ⊢ ( 𝐾 ∈ ℤ → ( ( 𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ↔ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) )
4 1 3 sylan9bb ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∈ ℤ ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) )
5 4 3impa ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) )
6 5 3comr ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁 ) ) )