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
2 1 ltp1i 1<1+1
3 df-2 2=1+1
4 2 3 breqtrri 1<2