Metamath Proof Explorer

Theorem nnne0i

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

Ref Expression
Hypothesis nngt0.1 
|- A e. NN
Assertion nnne0i 
|- A =/= 0

Proof

Step Hyp Ref Expression
1 nngt0.1 
 |-  A e. NN
2 1 nnrei 
 |-  A e. RR
3 1 nngt0i 
 |-  0 < A
4 2 3 gt0ne0ii 
 |-  A =/= 0