Metamath Proof Explorer


Theorem 9lt10

Description: 9 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015) (Revised by AV, 8-Sep-2021)

Ref Expression
Assertion 9lt10 9<10

Proof

Step Hyp Ref Expression
1 9re 9
2 1 ltp1i 9<9+1
3 9p1e10 9+1=10
4 2 3 breqtri 9<10