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

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 ⊢ 𝐴 𝐶 < 𝐵 𝐷