Metamath Proof Explorer


Theorem 7lt10

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

Ref Expression
Assertion 7lt10 7<10

Proof

Step Hyp Ref Expression
1 7lt8 7<8
2 8lt10 8<10
3 7re 7
4 8re 8
5 10re 10
6 3 4 5 lttri 7<88<107<10
7 1 2 6 mp2an 7<10