Metamath Proof Explorer


Theorem 10nn

Description: 10 is a positive integer. (Contributed by NM, 8-Nov-2012) (Revised by AV, 6-Sep-2021)

Ref Expression
Assertion 10nn
|- ; 1 0 e. NN

Proof

Step Hyp Ref Expression
1 9p1e10
 |-  ( 9 + 1 ) = ; 1 0
2 9nn
 |-  9 e. NN
3 peano2nn
 |-  ( 9 e. NN -> ( 9 + 1 ) e. NN )
4 2 3 ax-mp
 |-  ( 9 + 1 ) e. NN
5 1 4 eqeltrri
 |-  ; 1 0 e. NN