Theorem 1lt10

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

	Ref	Expression
Assertion	1lt10	⊢ 1 < ; 1 0

Proof

Step	Hyp	Ref	Expression
1		1nn0	⊢ 1 ∈ ℕ0
2		1re	⊢ 1 ∈ ℝ
3		9re	⊢ 9 ∈ ℝ
4		1lt9	⊢ 1 < 9
5	2 3 4	ltleii	⊢ 1 ≤ 9
6	1 5	le9lt10	⊢ 1 < ; 1 0