Metamath Proof Explorer

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 ⊢ M ∈ ℤ ∧ N ∈ ℤ → ¬ M < N ↔ M ..^ N = ∅

Proof

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