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