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=∅