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