Theorem dpltc

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

	Ref	Expression
Hypotheses	dpltc.a	$$⊢A\in {\mathbb{N}}_0$$
	dpltc.b	$$⊢B\in {ℝ}^{+}$$
	dpltc.c	$$⊢C\in {\mathbb{N}}_0$$
	dpltc.d	$$⊢D\in {ℝ}^{+}$$
	dpltc.1	$$⊢A<C$$
	dpltc.2	$$⊢B<10$$
Assertion	dpltc	$$⊢A.B<C.D$$

Proof

Step	Hyp	Ref	Expression
1		dpltc.a	$$⊢A\in {\mathbb{N}}_0$$
2		dpltc.b	$$⊢B\in {ℝ}^{+}$$
3		dpltc.c	$$⊢C\in {\mathbb{N}}_0$$
4		dpltc.d	$$⊢D\in {ℝ}^{+}$$
5		dpltc.1	$$⊢A<C$$
6		dpltc.2	$$⊢B<10$$
7	1 2 3 4 6 5	dp2ltc	Could not format _ A B < _ C D : No typesetting found for |- _ A B < _ C D with typecode |-
8	1 2	dpval3rp	Could not format ( A . B ) = _ A B : No typesetting found for |- ( A . B ) = _ A B with typecode |-
9	3 4	dpval3rp	Could not format ( C . D ) = _ C D : No typesetting found for |- ( C . D ) = _ C D with typecode |-
10	7 8 9	3brtr4i	$$⊢A.B<C.D$$