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

Metamath Proof Explorer

Theorem 4lt5

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

		Ref	Expression
	Assertion	4lt5	$⊢ 4 < 5$

Step	Hyp	Ref	Expression
1		4re	$⊢ 4 \in ℝ$
2	1	ltp1i	$⊢ 4 < 4 + 1$
3		df-5	$⊢ 5 = 4 + 1$
4	2 3	breqtrri	$⊢ 4 < 5$