Theorem 7lt10

Description: 7 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015) (Revised by AV, 8-Sep-2021) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026)

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

Proof

Step	Hyp	Ref	Expression
1		7nn0	$$⊢7\in {\mathbb{N}}_0$$
2		7re	$$⊢7\in ℝ$$
3		9re	$$⊢9\in ℝ$$
4		7lt9	$$⊢7<9$$
5	2 3 4	ltleii	$$⊢7\le 9$$
6	1 5	le9lt10	$$⊢7<10$$