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 ∈ ℝ
2	1	ltp1i	⊢ 4 < ( 4 + 1 )
3		df-5	⊢ 5 = ( 4 + 1 )
4	2 3	breqtrri	⊢ 4 < 5