Theorem 4lt5

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

	Ref	Expression
Assertion	4lt5	$$⊢4<5$$

Proof

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$$