Theorem eluzfz1

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

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

Proof

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