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