Metamath Proof Explorer


Theorem decleh

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

Ref Expression
Hypotheses decle.1 𝐴 ∈ ℕ0
decle.2 𝐵 ∈ ℕ0
decle.3 𝐶 ∈ ℕ0
decleh.4 𝐷 ∈ ℕ0
decleh.5 𝐶 ≤ 9
decleh.6 𝐴 < 𝐵
Assertion decleh 𝐴 𝐶 𝐵 𝐷

Proof

Step Hyp Ref Expression
1 decle.1 𝐴 ∈ ℕ0
2 decle.2 𝐵 ∈ ℕ0
3 decle.3 𝐶 ∈ ℕ0
4 decleh.4 𝐷 ∈ ℕ0
5 decleh.5 𝐶 ≤ 9
6 decleh.6 𝐴 < 𝐵
7 1 3 deccl 𝐴 𝐶 ∈ ℕ0
8 7 nn0rei 𝐴 𝐶 ∈ ℝ
9 2 4 deccl 𝐵 𝐷 ∈ ℕ0
10 9 nn0rei 𝐵 𝐷 ∈ ℝ
11 1 2 3 4 5 6 declth 𝐴 𝐶 < 𝐵 𝐷
12 8 10 11 ltleii 𝐴 𝐶 𝐵 𝐷