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