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

Metamath Proof Explorer

Theorem elfzo3

Description: Express membership in a half-open integer interval in terms of the "less than or equal to" and "less than" predicates on integers, resp. K e. ( ZZ>=M ) <-> M <_ K , K e. ( K ..^ N ) <-> K < N . (Contributed by Mario Carneiro, 29-Sep-2015)

Ref Expression
Assertion elfzo3 ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐾 ∈ ( 𝐾 ..^ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 3anass ⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) ↔ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) ) )
2 elfzo2 ⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) )
3 eluzelz ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝐾 ∈ ℤ )
4 fzolb ⊢ ( 𝐾 ∈ ( 𝐾 ..^ 𝑁 ) ↔ ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) )
5 3anass ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) ↔ ( 𝐾 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) ) )
6 4 5 bitri ⊢ ( 𝐾 ∈ ( 𝐾 ..^ 𝑁 ) ↔ ( 𝐾 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) ) )
7 6 baib ⊢ ( 𝐾 ∈ ℤ → ( 𝐾 ∈ ( 𝐾 ..^ 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) ) )
8 3 7 syl ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐾 ∈ ( 𝐾 ..^ 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) ) )
9 8 pm5.32i ⊢ ( ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐾 ∈ ( 𝐾 ..^ 𝑁 ) ) ↔ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑁 ∈ ℤ ∧ 𝐾 < 𝑁 ) ) )
10 1 2 9 3bitr4i ⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) ↔ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐾 ∈ ( 𝐾 ..^ 𝑁 ) ) )