Metamath Proof Explorer


Theorem 6lt7

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

Ref Expression
Assertion 6lt7
|- 6 < 7

Proof

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