Metamath Proof Explorer


Theorem declth

Description: Comparing two decimal integers (unequal higher places). (Contributed by AV, 8-Sep-2021)

Ref Expression
Hypotheses declt.a 𝐴 ∈ ℕ0
declt.b 𝐵 ∈ ℕ0
declth.c 𝐶 ∈ ℕ0
declth.d 𝐷 ∈ ℕ0
declth.e 𝐶 ≤ 9
declth.l 𝐴 < 𝐵
Assertion declth 𝐴 𝐶 < 𝐵 𝐷

Proof

Step Hyp Ref Expression
1 declt.a 𝐴 ∈ ℕ0
2 declt.b 𝐵 ∈ ℕ0
3 declth.c 𝐶 ∈ ℕ0
4 declth.d 𝐷 ∈ ℕ0
5 declth.e 𝐶 ≤ 9
6 declth.l 𝐴 < 𝐵
7 3 5 le9lt10 𝐶 < 1 0
8 1 2 3 4 7 6 decltc 𝐴 𝐶 < 𝐵 𝐷