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

Proof

Step	Hyp	Ref	Expression
1		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
2		zre	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
3		suble0	⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( ( 𝑁 − 𝑀 ) ≤ 0 ↔ 𝑁 ≤ 𝑀 ) )
4	1 2 3	syl2an	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝑁 − 𝑀 ) ≤ 0 ↔ 𝑁 ≤ 𝑀 ) )
5		0z	⊢ 0 ∈ ℤ
6		zsubcl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑁 − 𝑀 ) ∈ ℤ )
7		fzon	⊢ ( ( 0 ∈ ℤ ∧ ( 𝑁 − 𝑀 ) ∈ ℤ ) → ( ( 𝑁 − 𝑀 ) ≤ 0 ↔ ( 0 ..^ ( 𝑁 − 𝑀 ) ) = ∅ ) )
8	5 6 7	sylancr	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝑁 − 𝑀 ) ≤ 0 ↔ ( 0 ..^ ( 𝑁 − 𝑀 ) ) = ∅ ) )
9	4 8	bitr3d	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑁 ≤ 𝑀 ↔ ( 0 ..^ ( 𝑁 − 𝑀 ) ) = ∅ ) )
10	9	ancoms	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ≤ 𝑀 ↔ ( 0 ..^ ( 𝑁 − 𝑀 ) ) = ∅ ) )