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

Metamath Proof Explorer

Theorem 7lt8

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

Ref Expression
Assertion 7lt8 7 < 8

Proof

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