Metamath Proof Explorer


Theorem 2lt9

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

Ref Expression
Assertion 2lt9 2 < 9

Proof

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