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

Metamath Proof Explorer

Theorem dpltc

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

Ref Expression
Hypotheses dpltc.a ⊢ A ∈ ℕ 0
dpltc.b ⊢ B ∈ ℝ +
dpltc.c ⊢ C ∈ ℕ 0
dpltc.d ⊢ D ∈ ℝ +
dpltc.1 ⊢ A < C
dpltc.2 ⊢ B < 10
Assertion dpltc ⊢ A . B < C . D

Proof

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