fzn

Description: A finite set of sequential integers is empty if the bounds are reversed. (Contributed by NM, 22-Aug-2005)

		Ref	Expression
	Assertion	fzn	$⊢ (M \in ℤ \land N \in ℤ) \to (N < M \leftrightarrow (M \dots N) = \emptyset)$

Step	Hyp	Ref	Expression
1		fzn0	$⊢ (M \dots N) \neq \emptyset \leftrightarrow N \in ℤ_{\geq M}$
2		eluz	$⊢ (M \in ℤ \land N \in ℤ) \to (N \in ℤ_{\geq M} \leftrightarrow M \leq N)$
3	1 2	bitrid	$⊢ (M \in ℤ \land N \in ℤ) \to ((M \dots N) \neq \emptyset \leftrightarrow M \leq N)$
4		zre	$⊢ M \in ℤ \to M \in ℝ$
5		zre	$⊢ N \in ℤ \to N \in ℝ$
6		lenlt	$⊢ (M \in ℝ \land N \in ℝ) \to (M \leq N \leftrightarrow \neg N < M)$
7	4 5 6	syl2an	$⊢ (M \in ℤ \land N \in ℤ) \to (M \leq N \leftrightarrow \neg N < M)$
8	3 7	bitr2d	$⊢ (M \in ℤ \land N \in ℤ) \to (\neg N < M \leftrightarrow (M \dots N) \neq \emptyset)$
9	8	necon4bbid	$⊢ (M \in ℤ \land N \in ℤ) \to (N < M \leftrightarrow (M \dots N) = \emptyset)$

Metamath Proof Explorer