Metamath Proof Explorer
Description: Comparing two decimal integers (unequal higher places). (Contributed by AV, 8-Sep-2021)
|
|
Ref |
Expression |
|
Hypotheses |
declt.a |
|- A e. NN0 |
|
|
declt.b |
|- B e. NN0 |
|
|
declth.c |
|- C e. NN0 |
|
|
declth.d |
|- D e. NN0 |
|
|
declth.e |
|- C <_ 9 |
|
|
declth.l |
|- A < B |
|
Assertion |
declth |
|- ; A C < ; B D |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
declt.a |
|- A e. NN0 |
2 |
|
declt.b |
|- B e. NN0 |
3 |
|
declth.c |
|- C e. NN0 |
4 |
|
declth.d |
|- D e. NN0 |
5 |
|
declth.e |
|- C <_ 9 |
6 |
|
declth.l |
|- A < B |
7 |
3 5
|
le9lt10 |
|- C < ; 1 0 |
8 |
1 2 3 4 7 6
|
decltc |
|- ; A C < ; B D |