Metamath Proof Explorer


Theorem fzon0

Description: A half-open integer interval is nonempty iff it contains its left endpoint. (Contributed by Mario Carneiro, 29-Sep-2015)

Ref Expression
Assertion fzon0 ( ( 𝑀 ..^ 𝑁 ) ≠ ∅ ↔ 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 n0 ( ( 𝑀 ..^ 𝑁 ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝑀 ..^ 𝑁 ) )
2 elfzolt3b ( 𝑥 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) )
3 2 exlimiv ( ∃ 𝑥 𝑥 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) )
4 1 3 sylbi ( ( 𝑀 ..^ 𝑁 ) ≠ ∅ → 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) )
5 ne0i ( 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑀 ..^ 𝑁 ) ≠ ∅ )
6 4 5 impbii ( ( 𝑀 ..^ 𝑁 ) ≠ ∅ ↔ 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) )