Theorem eluz2b3

Description: Two ways to say "an integer greater than or equal to 2". (Contributed by Paul Chapman, 23-Nov-2012)

	Ref	Expression
Assertion	eluz2b3	$$⊢N\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(N\in \mathbb{N}\wedge N\ne 1\right)$$

Proof

Step	Hyp	Ref	Expression
1		eluz2b2	$$⊢N\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(N\in \mathbb{N}\wedge 1<N\right)$$
2		nngt1ne1	$$⊢N\in \mathbb{N}\to \left(1<N\leftrightarrow N\ne 1\right)$$
3	2	pm5.32i	$$⊢\left(N\in \mathbb{N}\wedge 1<N\right)\leftrightarrow \left(N\in \mathbb{N}\wedge N\ne 1\right)$$
4	1 3	bitri	$$⊢N\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(N\in \mathbb{N}\wedge N\ne 1\right)$$