This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ℕ \to (1 < A \leftrightarrow A \neq 1)$

Step	Hyp	Ref	Expression
1		1re	$⊢ 1 \in ℝ$
2		nnre	$⊢ A \in ℕ \to A \in ℝ$
3		nnge1	$⊢ A \in ℕ \to 1 \leq A$
4		leltne	$⊢ (1 \in ℝ \land A \in ℝ \land 1 \leq A) \to (1 < A \leftrightarrow A \neq 1)$
5	1 2 3 4	mp3an2i	$⊢ A \in ℕ \to (1 < A \leftrightarrow A \neq 1)$