This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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