Description: The number 0 is less than or equal to 2. (Contributed by David A. Wheeler, 7-Dec-2018) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 0le2 | |- 0 <_ 2 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0re | |- 0 e. RR |
|
| 2 | 2re | |- 2 e. RR |
|
| 3 | 2nn | |- 2 e. NN |
|
| 4 | 3 | nngt0i | |- 0 < 2 |
| 5 | 1 2 4 | ltleii | |- 0 <_ 2 |