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	⊢ ( ( 𝑀 ..^ 𝑁 ) ≠ ∅ ↔ 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) )