Theorem fzn0

Description: Properties of a finite interval of integers which is nonempty. (Contributed by Jeff Madsen, 17-Jun-2010) (Revised by Mario Carneiro, 28-Apr-2015)

	Ref	Expression
Assertion	fzn0	⊢ ( ( 𝑀 ... 𝑁 ) ≠ ∅ ↔ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		n0	⊢ ( ( 𝑀 ... 𝑁 ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝑀 ... 𝑁 ) )
2		elfzuz2	⊢ ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
3	2	exlimiv	⊢ ( ∃ 𝑥 𝑥 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
4	1 3	sylbi	⊢ ( ( 𝑀 ... 𝑁 ) ≠ ∅ → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
5		eluzfz1	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
6	5	ne0d	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 ... 𝑁 ) ≠ ∅ )
7	4 6	impbii	⊢ ( ( 𝑀 ... 𝑁 ) ≠ ∅ ↔ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )