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	$$⊢\left(M\dots N\right)\ne \varnothing \leftrightarrow N\in {\mathbb{Z}}_{\ge M}$$

Proof

Step	Hyp	Ref	Expression
1		n0	$$⊢\left(M\dots N\right)\ne \varnothing \leftrightarrow \exists xx\in \left(M\dots N\right)$$
2		elfzuz2	$$⊢x\in \left(M\dots N\right)\to N\in {\mathbb{Z}}_{\ge M}$$
3	2	exlimiv	$$⊢\exists xx\in \left(M\dots N\right)\to N\in {\mathbb{Z}}_{\ge M}$$
4	1 3	sylbi	$$⊢\left(M\dots N\right)\ne \varnothing \to N\in {\mathbb{Z}}_{\ge M}$$
5		eluzfz1	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\in \left(M\dots N\right)$$
6	5	ne0d	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(M\dots N\right)\ne \varnothing$$
7	4 6	impbii	$$⊢\left(M\dots N\right)\ne \varnothing \leftrightarrow N\in {\mathbb{Z}}_{\ge M}$$