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