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

Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 fzn0 ⊢ ( ( 𝑀 ... 𝑁 ) ≠ ∅ ↔ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
2 eluz ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑀 ≤ 𝑁 ) )
3 1 2 bitrid ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 ... 𝑁 ) ≠ ∅ ↔ 𝑀 ≤ 𝑁 ) )
4 zre ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
5 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
6 lenlt ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑀 ≤ 𝑁 ↔ ¬ 𝑁 < 𝑀 ) )
7 4 5 6 syl2an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ≤ 𝑁 ↔ ¬ 𝑁 < 𝑀 ) )
8 3 7 bitr2d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ¬ 𝑁 < 𝑀 ↔ ( 𝑀 ... 𝑁 ) ≠ ∅ ) )
9 8 necon4bbid ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 < 𝑀 ↔ ( 𝑀 ... 𝑁 ) = ∅ ) )