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

Metamath Proof Explorer

Theorem 1lt2

Description: 1 is less than 2. (Contributed by NM, 24-Feb-2005)

Ref Expression
Assertion 1lt2 
|- 1 < 2

Proof

Step Hyp Ref Expression
1 1re 
 |-  1 e. RR
2 1 ltp1i 
 |-  1 < ( 1 + 1 )
3 df-2 
 |-  2 = ( 1 + 1 )
4 2 3 breqtrri 
 |-  1 < 2