This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )