Metamath Proof Explorer
Description: Comparing two decimal integers (unequal higher places). (Contributed by Thierry Arnoux, 16-Dec-2021)
|
|
Ref |
Expression |
|
Hypotheses |
dpltc.a |
|- A e. NN0 |
|
|
dpltc.b |
|- B e. RR+ |
|
|
dpltc.c |
|- C e. NN0 |
|
|
dpltc.d |
|- D e. RR+ |
|
|
dpltc.1 |
|- A < C |
|
|
dpltc.2 |
|- B < ; 1 0 |
|
Assertion |
dpltc |
|- ( A . B ) < ( C . D ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
dpltc.a |
|- A e. NN0 |
2 |
|
dpltc.b |
|- B e. RR+ |
3 |
|
dpltc.c |
|- C e. NN0 |
4 |
|
dpltc.d |
|- D e. RR+ |
5 |
|
dpltc.1 |
|- A < C |
6 |
|
dpltc.2 |
|- B < ; 1 0 |
7 |
1 2 3 4 6 5
|
dp2ltc |
|- _ A B < _ C D |
8 |
1 2
|
dpval3rp |
|- ( A . B ) = _ A B |
9 |
3 4
|
dpval3rp |
|- ( C . D ) = _ C D |
10 |
7 8 9
|
3brtr4i |
|- ( A . B ) < ( C . D ) |