This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 1lt10

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

Ref Expression
Assertion 1lt10 ⊢ 1 < 10

Proof

Step Hyp Ref Expression
1 1lt2 ⊢ 1 < 2
2 2lt10 ⊢ 2 < 10
3 1re ⊢ 1 ∈ ℝ
4 2re ⊢ 2 ∈ ℝ
5 10re ⊢ 10 ∈ ℝ
6 3 4 5 lttri ⊢ 1 < 2 ∧ 2 < 10 → 1 < 10
7 1 2 6 mp2an ⊢ 1 < 10