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 ⊢ A ∈ ℕ 0
dplt.b ⊢ B ∈ ℝ +
dplt.d ⊢ C ∈ ℝ +
dplt.1 ⊢ B < C
Assertion dplt ⊢ A . B < A . C

Proof

Step Hyp Ref Expression
1 dplt.a ⊢ A ∈ ℕ 0
2 dplt.b ⊢ B ∈ ℝ +
3 dplt.d ⊢ C ∈ ℝ +
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