Metamath Proof Explorer


Theorem 5lt9

Description: 5 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015)

Ref Expression
Assertion 5lt9 5 < 9

Proof

Step Hyp Ref Expression
1 5lt6 5 < 6
2 6lt9 6 < 9
3 5re 5 ∈ ℝ
4 6re 6 ∈ ℝ
5 9re 9 ∈ ℝ
6 3 4 5 lttri ( ( 5 < 6 ∧ 6 < 9 ) → 5 < 9 )
7 1 2 6 mp2an 5 < 9