Metamath Proof Explorer


Theorem 8lt9

Description: 8 is less than 9. (Contributed by Mario Carneiro, 19-Feb-2014)

Ref Expression
Assertion 8lt9 8<9

Proof

Step Hyp Ref Expression
1 8re 8
2 1 ltp1i 8<8+1
3 df-9 9=8+1
4 2 3 breqtrri 8<9