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

Metamath Proof Explorer

Theorem 5lt6

Description: 5 is less than 6. (Contributed by Mario Carneiro, 15-Sep-2013)

Ref Expression
Assertion 5lt6 5 < 6

Proof

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