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

Metamath Proof Explorer

Theorem 1lt2

Description: 1 is less than 2. (Contributed by NM, 24-Feb-2005)

Ref Expression
Assertion 1lt2 1 < 2

Proof

Step Hyp Ref Expression
1 1re ⊢ 1 ∈ ℝ
2 1 ltp1i ⊢ 1 < ( 1 + 1 )
3 df-2 ⊢ 2 = ( 1 + 1 )
4 2 3 breqtrri ⊢ 1 < 2