Metamath Proof Explorer

Theorem decltc

Description: Comparing two decimal integers (unequal higher places). (Contributed by Mario Carneiro, 18-Feb-2014) (Revised by AV, 6-Sep-2021)

Ref Expression
Hypotheses declt.a ⊢ 𝐴 ∈ ℕ0
declt.b ⊢ 𝐵 ∈ ℕ0
decltc.c ⊢ 𝐶 ∈ ℕ0
decltc.d ⊢ 𝐷 ∈ ℕ0
decltc.s ⊢ 𝐶 < 1 0
decltc.l ⊢ 𝐴 < 𝐵
Assertion decltc 𝐴 𝐶 < 𝐵 𝐷

Proof

Step Hyp Ref Expression
1 declt.a ⊢ 𝐴 ∈ ℕ0
2 declt.b ⊢ 𝐵 ∈ ℕ0
3 decltc.c ⊢ 𝐶 ∈ ℕ0
4 decltc.d ⊢ 𝐷 ∈ ℕ0
5 decltc.s ⊢ 𝐶 < 1 0
6 decltc.l ⊢ 𝐴 < 𝐵
7 10nn ⊢ 1 0 ∈ ℕ
8 7 1 2 3 4 5 6 numltc ⊢ ( ( 1 0 · 𝐴 ) + 𝐶 ) < ( ( 1 0 · 𝐵 ) + 𝐷 )
9 dfdec10 ⊢ 𝐴 𝐶 = ( ( 1 0 · 𝐴 ) + 𝐶 )
10 dfdec10 ⊢ 𝐵 𝐷 = ( ( 1 0 · 𝐵 ) + 𝐷 )
11 8 9 10 3brtr4i ⊢ 𝐴 𝐶 < 𝐵 𝐷