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 |