fzo0n

Description: A half-open range of nonnegative integers is empty iff the upper bound is not positive. (Contributed by AV, 2-May-2020)

		Ref	Expression
	Assertion	fzo0n	$⊢ (M \in ℤ \land N \in ℤ) \to (N \leq M \leftrightarrow (0 ..^N - M) = \emptyset)$

Step	Hyp	Ref	Expression
1		zre	$⊢ N \in ℤ \to N \in ℝ$
2		zre	$⊢ M \in ℤ \to M \in ℝ$
3		suble0	$⊢ (N \in ℝ \land M \in ℝ) \to (N - M \leq 0 \leftrightarrow N \leq M)$
4	1 2 3	syl2an	$⊢ (N \in ℤ \land M \in ℤ) \to (N - M \leq 0 \leftrightarrow N \leq M)$
5		0z	$⊢ 0 \in ℤ$
6		zsubcl	$⊢ (N \in ℤ \land M \in ℤ) \to N - M \in ℤ$
7		fzon	$⊢ (0 \in ℤ \land N - M \in ℤ) \to (N - M \leq 0 \leftrightarrow (0 ..^N - M) = \emptyset)$
8	5 6 7	sylancr	$⊢ (N \in ℤ \land M \in ℤ) \to (N - M \leq 0 \leftrightarrow (0 ..^N - M) = \emptyset)$
9	4 8	bitr3d	$⊢ (N \in ℤ \land M \in ℤ) \to (N \leq M \leftrightarrow (0 ..^N - M) = \emptyset)$
10	9	ancoms	$⊢ (M \in ℤ \land N \in ℤ) \to (N \leq M \leftrightarrow (0 ..^N - M) = \emptyset)$

Metamath Proof Explorer