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 ⊢ 𝐴 ∈ ℕ0
dpltc.b ⊢ 𝐵 ∈ ℝ+
dpltc.c ⊢ 𝐶 ∈ ℕ0
dpltc.d ⊢ 𝐷 ∈ ℝ+
dpltc.1 ⊢ 𝐴 < 𝐶
dpltc.2 ⊢ 𝐵 < 1 0
Assertion dpltc ( 𝐴 . 𝐵 ) < ( 𝐶 . 𝐷 )

Proof

Step Hyp Ref Expression
1 dpltc.a ⊢ 𝐴 ∈ ℕ0
2 dpltc.b ⊢ 𝐵 ∈ ℝ+
3 dpltc.c ⊢ 𝐶 ∈ ℕ0
4 dpltc.d ⊢ 𝐷 ∈ ℝ+
5 dpltc.1 ⊢ 𝐴 < 𝐶
6 dpltc.2 ⊢ 𝐵 < 1 0
7 1 2 3 4 6 5 dp2ltc ⊢ 𝐴 𝐵 < 𝐶 𝐷
8 1 2 dpval3rp ⊢ ( 𝐴 . 𝐵 ) = 𝐴 𝐵
9 3 4 dpval3rp ⊢ ( 𝐶 . 𝐷 ) = 𝐶 𝐷
10 7 8 9 3brtr4i ⊢ ( 𝐴 . 𝐵 ) < ( 𝐶 . 𝐷 )