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 )