Theorem eluzfz2

Description: Membership in a finite set of sequential integers - special case. (Contributed by NM, 13-Sep-2005) (Revised by Mario Carneiro, 28-Apr-2015)

	Ref	Expression
Assertion	eluzfz2	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in \left(M\dots N\right)$$

Proof

Step	Hyp	Ref	Expression
1		eluzelz	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in \mathbb{Z}$$
2		uzid	$$⊢N\in \mathbb{Z}\to N\in {\mathbb{Z}}_{\ge N}$$
3	1 2	syl	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in {\mathbb{Z}}_{\ge N}$$
4		eluzfz	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge N\in {\mathbb{Z}}_{\ge N}\right)\to N\in \left(M\dots N\right)$$
5	3 4	mpdan	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in \left(M\dots N\right)$$