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 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 1nn0 | |- 1 e. NN0 |
|
| 2 | 1re | |- 1 e. RR |
|
| 3 | 9re | |- 9 e. RR |
|
| 4 | 1lt9 | |- 1 < 9 |
|
| 5 | 2 3 4 | ltleii | |- 1 <_ 9 |
| 6 | 1 5 | le9lt10 | |- 1 < ; 1 0 |