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

Metamath Proof Explorer

Theorem dplt

Description: Comparing two decimal expansions (equal higher places). (Contributed by Thierry Arnoux, 16-Dec-2021)

Ref Expression
Hypotheses dplt.a 
|- A e. NN0
dplt.b 
|- B e. RR+
dplt.d 
|- C e. RR+
dplt.1 
|- B < C
Assertion dplt 
|- ( A . B ) < ( A . C )

Proof

Step Hyp Ref Expression
1 dplt.a 
 |-  A e. NN0
2 dplt.b 
 |-  B e. RR+
3 dplt.d 
 |-  C e. RR+
4 dplt.1 
 |-  B < C
5 1 2 3 4 dp2lt 
 |-  _ A B < _ A C
6 1 2 dpval3rp 
 |-  ( A . B ) = _ A B
7 1 3 dpval3rp 
 |-  ( A . C ) = _ A C
8 5 6 7 3brtr4i 
 |-  ( A . B ) < ( A . C )