Theorem eluz1i

Description: Membership in an upper set of integers. (Contributed by NM, 5-Sep-2005)

	Ref	Expression
Hypothesis	eluz.1	$$⊢M\in \mathbb{Z}$$
Assertion	eluz1i	$$⊢N\in {\mathbb{Z}}_{\ge M}\leftrightarrow \left(N\in \mathbb{Z}\wedge M\le N\right)$$

Proof

Step	Hyp	Ref	Expression
1		eluz.1	$$⊢M\in \mathbb{Z}$$
2		eluz1	$$⊢M\in \mathbb{Z}\to \left(N\in {\mathbb{Z}}_{\ge M}\leftrightarrow \left(N\in \mathbb{Z}\wedge M\le N\right)\right)$$
3	1 2	ax-mp	$$⊢N\in {\mathbb{Z}}_{\ge M}\leftrightarrow \left(N\in \mathbb{Z}\wedge M\le N\right)$$