Theorem fzonlt0

Description: A half-open integer range is empty if the bounds are equal or reversed. (Contributed by AV, 20-Oct-2018)

	Ref	Expression
Assertion	fzonlt0	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ¬ 𝑀 < 𝑁 ↔ ( 𝑀 ..^ 𝑁 ) = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
2		zre	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
3		lenlt	⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( 𝑁 ≤ 𝑀 ↔ ¬ 𝑀 < 𝑁 ) )
4	1 2 3	syl2anr	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ≤ 𝑀 ↔ ¬ 𝑀 < 𝑁 ) )
5		fzon	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ≤ 𝑀 ↔ ( 𝑀 ..^ 𝑁 ) = ∅ ) )
6	4 5	bitr3d	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ¬ 𝑀 < 𝑁 ↔ ( 𝑀 ..^ 𝑁 ) = ∅ ) )