Description: Comparing a digit to a decimal integer. (Contributed by AV, 8-Sep-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | declti.a | |- A e. NN |
|
declti.b | |- B e. NN0 |
||
declti.c | |- C e. NN0 |
||
decltdi.4 | |- C <_ 9 |
||
Assertion | decltdi | |- C < ; A B |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | declti.a | |- A e. NN |
|
2 | declti.b | |- B e. NN0 |
|
3 | declti.c | |- C e. NN0 |
|
4 | decltdi.4 | |- C <_ 9 |
|
5 | 3 4 | le9lt10 | |- C < ; 1 0 |
6 | 1 2 3 5 | declti | |- C < ; A B |