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	⊢ ( 𝐴 ∈ ℕ → ( 1 < 𝐴 ↔ 𝐴 ≠ 1 ) )

Proof

Step	Hyp	Ref	Expression
1		1re	⊢ 1 ∈ ℝ
2		nnre	⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℝ )
3		nnge1	⊢ ( 𝐴 ∈ ℕ → 1 ≤ 𝐴 )
4		leltne	⊢ ( ( 1 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( 1 < 𝐴 ↔ 𝐴 ≠ 1 ) )
5	1 2 3 4	mp3an2i	⊢ ( 𝐴 ∈ ℕ → ( 1 < 𝐴 ↔ 𝐴 ≠ 1 ) )