# Metamath Proof Explorer

## Theorem declt

Description: Comparing two decimal integers (equal higher places). (Contributed by Mario Carneiro, 17-Apr-2015) (Revised by AV, 6-Sep-2021)

Ref Expression
Hypotheses declt.a ${⊢}{A}\in {ℕ}_{0}$
declt.b ${⊢}{B}\in {ℕ}_{0}$
declt.c ${⊢}{C}\in ℕ$
declt.l ${⊢}{B}<{C}$
Assertion declt Could not format assertion : No typesetting found for |- ; A B < ; A C with typecode |-

### Proof

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