Theorem 9lt10

Description: 9 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015) (Revised by AV, 8-Sep-2021)

	Ref	Expression
Assertion	9lt10	$$⊢9<10$$

Proof

Step	Hyp	Ref	Expression
1		9re	$$⊢9\in ℝ$$
2	1	ltp1i	$$⊢9<9+1$$
3		9p1e10	$$⊢9+1=10$$
4	2 3	breqtri	$$⊢9<10$$