This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ≤ 𝑀 ↔ ( 𝑀 ..^ 𝑁 ) = ∅ ) )

Proof

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