Description: A "decimal digit" (i.e. a nonnegative integer less than or equal to 9) is less then 10. (Contributed by AV, 8-Sep-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | le9lt10.c | |- A e. NN0 |
|
| le9lt10.e | |- A <_ 9 |
||
| Assertion | le9lt10 | |- A < ; 1 0 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | le9lt10.c | |- A e. NN0 |
|
| 2 | le9lt10.e | |- A <_ 9 |
|
| 3 | 1 | nn0zi | |- A e. ZZ |
| 4 | 9nn0 | |- 9 e. NN0 |
|
| 5 | 4 | nn0zi | |- 9 e. ZZ |
| 6 | zleltp1 | |- ( ( A e. ZZ /\ 9 e. ZZ ) -> ( A <_ 9 <-> A < ( 9 + 1 ) ) ) |
|
| 7 | 3 5 6 | mp2an | |- ( A <_ 9 <-> A < ( 9 + 1 ) ) |
| 8 | 2 7 | mpbi | |- A < ( 9 + 1 ) |
| 9 | 9p1e10 | |- ( 9 + 1 ) = ; 1 0 |
|
| 10 | 8 9 | breqtri | |- A < ; 1 0 |