Metamath Proof Explorer


Theorem dpltc

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 )