# 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 ${⊢}{A}\in {ℕ}_{0}$
declt.b ${⊢}{B}\in {ℕ}_{0}$
decltc.c ${⊢}{C}\in {ℕ}_{0}$
decltc.d ${⊢}{D}\in {ℕ}_{0}$
decltc.s ${⊢}{C}<10$
decltc.l ${⊢}{A}<{B}$
Assertion decltc Could not format assertion : No typesetting found for |- ; A C < ; B D with typecode |-

### Proof

Step Hyp Ref Expression
1 declt.a ${⊢}{A}\in {ℕ}_{0}$
2 declt.b ${⊢}{B}\in {ℕ}_{0}$
3 decltc.c ${⊢}{C}\in {ℕ}_{0}$
4 decltc.d ${⊢}{D}\in {ℕ}_{0}$
5 decltc.s ${⊢}{C}<10$
6 decltc.l ${⊢}{A}<{B}$
7 10nn ${⊢}10\in ℕ$
8 7 1 2 3 4 5 6 numltc ${⊢}10{A}+{C}<10{B}+{D}$
9 dfdec10 Could not format ; A C = ( ( ; 1 0 x. A ) + C ) : No typesetting found for |- ; A C = ( ( ; 1 0 x. A ) + C ) with typecode |-
10 dfdec10 Could not format ; B D = ( ( ; 1 0 x. B ) + D ) : No typesetting found for |- ; B D = ( ( ; 1 0 x. B ) + D ) with typecode |-
11 8 9 10 3brtr4i Could not format ; A C < ; B D : No typesetting found for |- ; A C < ; B D with typecode |-