Metamath Proof Explorer

Theorem fzon

Description: A half-open set of sequential integers is empty if the bounds are equal or reversed. (Contributed by Alexander van der Vekens, 30-Oct-2017)

Ref Expression
Assertion fzon ⊢ M ∈ ℤ ∧ N ∈ ℤ → N ≤ M ↔ M ..^ N = ∅

Proof

Step Hyp Ref Expression
1 peano2zm ⊢ N ∈ ℤ → N − 1 ∈ ℤ
2 fzn ⊢ M ∈ ℤ ∧ N − 1 ∈ ℤ → N − 1 < M ↔ M … N − 1 = ∅
3 1 2 sylan2 ⊢ M ∈ ℤ ∧ N ∈ ℤ → N − 1 < M ↔ M … N − 1 = ∅
4 zlem1lt ⊢ N ∈ ℤ ∧ M ∈ ℤ → N ≤ M ↔ N − 1 < M
5 4 ancoms ⊢ M ∈ ℤ ∧ N ∈ ℤ → N ≤ M ↔ N − 1 < M
6 fzoval ⊢ N ∈ ℤ → M ..^ N = M … N − 1
7 6 adantl ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ..^ N = M … N − 1
8 7 eqeq1d ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ..^ N = ∅ ↔ M … N − 1 = ∅
9 3 5 8 3bitr4d ⊢ M ∈ ℤ ∧ N ∈ ℤ → N ≤ M ↔ M ..^ N = ∅