Theorem eluz2gt1

Description: An integer greater than or equal to 2 is greater than 1. (Contributed by AV, 24-May-2020)

	Ref	Expression
Assertion	eluz2gt1	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 1<N$$

Proof

Step	Hyp	Ref	Expression
1		eluz2b1	$$⊢N\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(N\in \mathbb{Z}\wedge 1<N\right)$$
2	1	simprbi	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 1<N$$