Metamath Proof Explorer
Description: Comparing a digit to a decimal integer. (Contributed by AV, 17-Aug-2021)
|
|
Ref |
Expression |
|
Hypotheses |
declei.1 |
|- A e. NN |
|
|
declei.2 |
|- B e. NN0 |
|
|
declei.3 |
|- C e. NN0 |
|
|
declei.4 |
|- C <_ 9 |
|
Assertion |
declei |
|- C <_ ; A B |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
declei.1 |
|- A e. NN |
2 |
|
declei.2 |
|- B e. NN0 |
3 |
|
declei.3 |
|- C e. NN0 |
4 |
|
declei.4 |
|- C <_ 9 |
5 |
3
|
dec0h |
|- C = ; 0 C |
6 |
|
0nn0 |
|- 0 e. NN0 |
7 |
1
|
nnnn0i |
|- A e. NN0 |
8 |
1
|
nngt0i |
|- 0 < A |
9 |
6 7 3 2 4 8
|
decleh |
|- ; 0 C <_ ; A B |
10 |
5 9
|
eqbrtri |
|- C <_ ; A B |