This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: Comparing two decimal integers (unequal higher places). (Contributed by AV, 17-Aug-2021) (Revised by AV, 8-Sep-2021)
|
|
Ref |
Expression |
|
Hypotheses |
decle.1 |
|- A e. NN0 |
|
|
decle.2 |
|- B e. NN0 |
|
|
decle.3 |
|- C e. NN0 |
|
|
decleh.4 |
|- D e. NN0 |
|
|
decleh.5 |
|- C <_ 9 |
|
|
decleh.6 |
|- A < B |
|
Assertion |
decleh |
|- ; A C <_ ; B D |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
decle.1 |
|- A e. NN0 |
| 2 |
|
decle.2 |
|- B e. NN0 |
| 3 |
|
decle.3 |
|- C e. NN0 |
| 4 |
|
decleh.4 |
|- D e. NN0 |
| 5 |
|
decleh.5 |
|- C <_ 9 |
| 6 |
|
decleh.6 |
|- A < B |
| 7 |
1 3
|
deccl |
|- ; A C e. NN0 |
| 8 |
7
|
nn0rei |
|- ; A C e. RR |
| 9 |
2 4
|
deccl |
|- ; B D e. NN0 |
| 10 |
9
|
nn0rei |
|- ; B D e. RR |
| 11 |
1 2 3 4 5 6
|
declth |
|- ; A C < ; B D |
| 12 |
8 10 11
|
ltleii |
|- ; A C <_ ; B D |