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 < ; 1 0

Proof

Step	Hyp	Ref	Expression
1		9re	⊢ 9 ∈ ℝ
2	1	ltp1i	⊢ 9 < ( 9 + 1 )
3		9p1e10	⊢ ( 9 + 1 ) = ; 1 0
4	2 3	breqtri	⊢ 9 < ; 1 0