Metamath Proof Explorer


Theorem 5lt10

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

Ref Expression
Assertion 5lt10 5<10

Proof

Step Hyp Ref Expression
1 5lt6 5<6
2 6lt10 6<10
3 5re 5
4 6re 6
5 10re 10
6 3 4 5 lttri 5<66<105<10
7 1 2 6 mp2an 5<10