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

Metamath Proof Explorer

Theorem nngt0

Description: A positive integer is positive. (Contributed by NM, 26-Sep-1999)

Ref Expression
Assertion nngt0 ⊢ A ∈ ℕ → 0 < A

Proof

Step Hyp Ref Expression
1 nnre ⊢ A ∈ ℕ → A ∈ ℝ
2 nnge1 ⊢ A ∈ ℕ → 1 ≤ A
3 0lt1 ⊢ 0 < 1
4 0re ⊢ 0 ∈ ℝ
5 1re ⊢ 1 ∈ ℝ
6 ltletr ⊢ 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ A ∈ ℝ → 0 < 1 ∧ 1 ≤ A → 0 < A
7 4 5 6 mp3an12 ⊢ A ∈ ℝ → 0 < 1 ∧ 1 ≤ A → 0 < A
8 3 7 mpani ⊢ A ∈ ℝ → 1 ≤ A → 0 < A
9 1 2 8 sylc ⊢ A ∈ ℕ → 0 < A