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

Metamath Proof Explorer

Theorem 10pos

Description: The number 10 is positive. (Contributed by NM, 5-Feb-2007) (Revised by AV, 8-Sep-2021)

Ref Expression
Assertion 10pos 
|- 0 < ; 1 0

Proof

Step Hyp Ref Expression
1 10nn 
 |-  ; 1 0 e. NN
2 1 nngt0i 
 |-  0 < ; 1 0