Metamath Proof Explorer

Theorem 1lt2pi

Description: One is less than two (one plus one). (Contributed by NM, 13-Mar-1996) (New usage is discouraged.)

Ref Expression
Assertion 1lt2pi 
|- 1o

Proof

Step Hyp Ref Expression
1 1onn 
 |-  1o e. _om
2 nna0 
 |-  ( 1o e. _om -> ( 1o +o (/) ) = 1o )
3 1 2 ax-mp 
 |-  ( 1o +o (/) ) = 1o
4 0lt1o 
 |-  (/) e. 1o
5 peano1 
 |-  (/) e. _om
6 nnaord 
 |-  ( ( (/) e. _om /\ 1o e. _om /\ 1o e. _om ) -> ( (/) e. 1o <-> ( 1o +o (/) ) e. ( 1o +o 1o ) ) )
7 5 1 1 6 mp3an 
 |-  ( (/) e. 1o <-> ( 1o +o (/) ) e. ( 1o +o 1o ) )
8 4 7 mpbi 
 |-  ( 1o +o (/) ) e. ( 1o +o 1o )
9 3 8 eqeltrri 
 |-  1o e. ( 1o +o 1o )
10 1pi 
 |-  1o e. N.
11 addpiord 
 |-  ( ( 1o e. N. /\ 1o e. N. ) -> ( 1o +N 1o ) = ( 1o +o 1o ) )
12 10 10 11 mp2an 
 |-  ( 1o +N 1o ) = ( 1o +o 1o )
13 9 12 eleqtrri 
 |-  1o e. ( 1o +N 1o )
14 addclpi 
 |-  ( ( 1o e. N. /\ 1o e. N. ) -> ( 1o +N 1o ) e. N. )
15 10 10 14 mp2an 
 |-  ( 1o +N 1o ) e. N.
16 ltpiord 
 |-  ( ( 1o e. N. /\ ( 1o +N 1o ) e. N. ) -> ( 1o  1o e. ( 1o +N 1o ) ) )
17 10 15 16 mp2an 
 |-  ( 1o  1o e. ( 1o +N 1o ) )
18 13 17 mpbir 
 |-  1o