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 | |
|
le9lt10.e | |
||
Assertion | le9lt10 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | le9lt10.c | |
|
2 | le9lt10.e | |
|
3 | 1 | nn0zi | |
4 | 9nn0 | |
|
5 | 4 | nn0zi | |
6 | zleltp1 | |
|
7 | 3 5 6 | mp2an | |
8 | 2 7 | mpbi | |
9 | 9p1e10 | |
|
10 | 8 9 | breqtri | |