Metamath Proof Explorer

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 ⊢ M ∈ ℤ ∧ N ∈ ℤ → N ≤ M ↔ 0 ..^ N − M = ∅

Proof

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