Theorem dplt

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

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

Proof

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