Metamath Proof Explorer
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 |
⊢ ; 𝐴 𝐶 ≤ ; 𝐵 𝐷 |