Metamath Proof Explorer

Theorem 3decltc

Description: Comparing two decimal integers with three "digits" (unequal higher places). (Contributed by AV, 15-Jun-2021) (Revised by AV, 6-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 ⊢ 𝐴 < 𝐵
3decltc.1 ⊢ 𝐶 < 1 0
3decltc.2 ⊢ 𝐸 < 1 0
Assertion 3decltc 𝐴 𝐶 𝐸 < 𝐵 𝐷 𝐹

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 3decltc.1 ⊢ 𝐶 < 1 0
9 3decltc.2 ⊢ 𝐸 < 1 0
10 1 3 deccl ⊢ 𝐴 𝐶 ∈ ℕ0
11 2 4 deccl ⊢ 𝐵 𝐷 ∈ ℕ0
12 1 2 3 4 8 7 decltc ⊢ 𝐴 𝐶 < 𝐵 𝐷
13 10 11 5 6 9 12 decltc ⊢ 𝐴 𝐶 𝐸 < 𝐵 𝐷 𝐹