This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐴 . 𝐵 ) < ( 𝐴 . 𝐶 )