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 )