Theorem dplt

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

	Ref	Expression
Hypotheses	dplt.a	⊢ 𝐴 ∈ ℕ0
	dplt.b	⊢ 𝐵 ∈ ℝ+
	dplt.d	⊢ 𝐶 ∈ ℝ+
	dplt.1	⊢ 𝐵 < 𝐶
Assertion	dplt	⊢ ( 𝐴 . 𝐵 ) < ( 𝐴 . 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		dplt.a	⊢ 𝐴 ∈ ℕ0
2		dplt.b	⊢ 𝐵 ∈ ℝ+
3		dplt.d	⊢ 𝐶 ∈ ℝ+
4		dplt.1	⊢ 𝐵 < 𝐶
5	1 2 3 4	dp2lt	⊢ _ 𝐴 𝐵 < _ 𝐴 𝐶
6	1 2	dpval3rp	⊢ ( 𝐴 . 𝐵 ) = _ 𝐴 𝐵
7	1 3	dpval3rp	⊢ ( 𝐴 . 𝐶 ) = _ 𝐴 𝐶
8	5 6 7	3brtr4i	⊢ ( 𝐴 . 𝐵 ) < ( 𝐴 . 𝐶 )