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 with three "digits" (unequal higher
places). (Contributed by AV, 15-Jun-2021) (Revised by AV, 6-Sep-2021)
|
|
Ref |
Expression |
|
Hypotheses |
3decltc.a |
|- A e. NN0 |
|
|
3decltc.b |
|- B e. NN0 |
|
|
3decltc.c |
|- C e. NN0 |
|
|
3decltc.d |
|- D e. NN0 |
|
|
3decltc.e |
|- E e. NN0 |
|
|
3decltc.f |
|- F e. NN0 |
|
|
3decltc.3 |
|- A < B |
|
|
3decltc.1 |
|- C < ; 1 0 |
|
|
3decltc.2 |
|- E < ; 1 0 |
|
Assertion |
3decltc |
|- ; ; A C E < ; ; B D F |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
3decltc.a |
|- A e. NN0 |
| 2 |
|
3decltc.b |
|- B e. NN0 |
| 3 |
|
3decltc.c |
|- C e. NN0 |
| 4 |
|
3decltc.d |
|- D e. NN0 |
| 5 |
|
3decltc.e |
|- E e. NN0 |
| 6 |
|
3decltc.f |
|- F e. NN0 |
| 7 |
|
3decltc.3 |
|- A < B |
| 8 |
|
3decltc.1 |
|- C < ; 1 0 |
| 9 |
|
3decltc.2 |
|- E < ; 1 0 |
| 10 |
1 3
|
deccl |
|- ; A C e. NN0 |
| 11 |
2 4
|
deccl |
|- ; B D e. NN0 |
| 12 |
1 2 3 4 8 7
|
decltc |
|- ; A C < ; B D |
| 13 |
10 11 5 6 9 12
|
decltc |
|- ; ; A C E < ; ; B D F |