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 \in ℤ \land N \in ℤ) \to (\neg M < N \leftrightarrow (M ..^N) = \emptyset)$

Step	Hyp	Ref	Expression
1		zre	$⊢ N \in ℤ \to N \in ℝ$
2		zre	$⊢ M \in ℤ \to M \in ℝ$
3		lenlt	$⊢ (N \in ℝ \land M \in ℝ) \to (N \leq M \leftrightarrow \neg M < N)$
4	1 2 3	syl2anr	$⊢ (M \in ℤ \land N \in ℤ) \to (N \leq M \leftrightarrow \neg M < N)$
5		fzon	$⊢ (M \in ℤ \land N \in ℤ) \to (N \leq M \leftrightarrow (M ..^N) = \emptyset)$
6	4 5	bitr3d	$⊢ (M \in ℤ \land N \in ℤ) \to (\neg M < N \leftrightarrow (M ..^N) = \emptyset)$

Metamath Proof Explorer