Theorem nnne1ge2

Description: A positive integer which is not 1 is greater than or equal to 2. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	nnne1ge2	$$⊢\left(N\in \mathbb{N}\wedge N\ne 1\right)\to 2\le N$$

Proof

Step	Hyp	Ref	Expression
1		nnnn0	$$⊢N\in \mathbb{N}\to N\in {\mathbb{N}}_0$$
2	1	adantr	$$⊢\left(N\in \mathbb{N}\wedge N\ne 1\right)\to N\in {\mathbb{N}}_0$$
3		nnne0	$$⊢N\in \mathbb{N}\to N\ne 0$$
4	3	adantr	$$⊢\left(N\in \mathbb{N}\wedge N\ne 1\right)\to N\ne 0$$
5		simpr	$$⊢\left(N\in \mathbb{N}\wedge N\ne 1\right)\to N\ne 1$$
6		nn0n0n1ge2	$$⊢\left(N\in {\mathbb{N}}_0\wedge N\ne 0\wedge N\ne 1\right)\to 2\le N$$
7	2 4 5 6	syl3anc	$$⊢\left(N\in \mathbb{N}\wedge N\ne 1\right)\to 2\le N$$