Metamath Proof Explorer

Theorem 3declth

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

Ref Expression
Hypotheses 3decltc.a ⊢ 𝐴 ∈ ℕ0
3decltc.b ⊢ 𝐵 ∈ ℕ0
3decltc.c ⊢ 𝐶 ∈ ℕ0
3decltc.d ⊢ 𝐷 ∈ ℕ0
3decltc.e ⊢ 𝐸 ∈ ℕ0
3decltc.f ⊢ 𝐹 ∈ ℕ0
3decltc.3 ⊢ 𝐴 < 𝐵
3declth.1 ⊢ 𝐶 ≤ 9
3declth.2 ⊢ 𝐸 ≤ 9
Assertion 3declth 𝐴 𝐶 𝐸 < 𝐵 𝐷 𝐹

Proof

Step Hyp Ref Expression
1 3decltc.a ⊢ 𝐴 ∈ ℕ0
2 3decltc.b ⊢ 𝐵 ∈ ℕ0
3 3decltc.c ⊢ 𝐶 ∈ ℕ0
4 3decltc.d ⊢ 𝐷 ∈ ℕ0
5 3decltc.e ⊢ 𝐸 ∈ ℕ0
6 3decltc.f ⊢ 𝐹 ∈ ℕ0
7 3decltc.3 ⊢ 𝐴 < 𝐵
8 3declth.1 ⊢ 𝐶 ≤ 9
9 3declth.2 ⊢ 𝐸 ≤ 9
10 1 3 deccl ⊢ 𝐴 𝐶 ∈ ℕ0
11 2 4 deccl ⊢ 𝐵 𝐷 ∈ ℕ0
12 1 2 3 4 8 7 declth ⊢ 𝐴 𝐶 < 𝐵 𝐷
13 10 11 5 6 9 12 declth ⊢ 𝐴 𝐶 𝐸 < 𝐵 𝐷 𝐹