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

Metamath Proof Explorer

Theorem nnne0i

Description: A positive integer is nonzero (inference version). (Contributed by NM, 25-Aug-1999)

Ref Expression
Hypothesis nngt0.1 ⊢ 𝐴 ∈ ℕ
Assertion nnne0i 𝐴 ≠ 0

Proof

Step Hyp Ref Expression
1 nngt0.1 ⊢ 𝐴 ∈ ℕ
2 1 nnrei ⊢ 𝐴 ∈ ℝ
3 1 nngt0i ⊢ 0 < 𝐴
4 2 3 gt0ne0ii ⊢ 𝐴 ≠ 0