Metamath Proof Explorer

Theorem 7lt8

Description: 7 is less than 8. (Contributed by Mario Carneiro, 15-Sep-2013)

Ref Expression
Assertion 7lt8 
|- 7 < 8

Proof

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