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 ( 𝐴 ∈ ℕ → ( 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 ) )