Theorem nngt1ne1

Description: A positive integer is greater than one iff it is not equal to one. (Contributed by NM, 7-Oct-2004)

	Ref	Expression
Assertion	nngt1ne1	$$⊢A\in \mathbb{N}\to \left(1<A\leftrightarrow A\ne 1\right)$$

Proof

Step	Hyp	Ref	Expression
1		1re	$$⊢1\in ℝ$$
2		nnre	$$⊢A\in \mathbb{N}\to A\in ℝ$$
3		nnge1	$$⊢A\in \mathbb{N}\to 1\le A$$
4		leltne	$$⊢\left(1\in ℝ\wedge A\in ℝ\wedge 1\le A\right)\to \left(1<A\leftrightarrow A\ne 1\right)$$
5	1 2 3 4	mp3an2i	$$⊢A\in \mathbb{N}\to \left(1<A\leftrightarrow A\ne 1\right)$$