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 ∈ ℕ
2 1 nngt0i 0 < 1 0