Metamath Proof Explorer


Theorem declth

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

Ref Expression
Hypotheses declt.a
|- A e. NN0
declt.b
|- B e. NN0
declth.c
|- C e. NN0
declth.d
|- D e. NN0
declth.e
|- C <_ 9
declth.l
|- A < B
Assertion declth
|- ; A C < ; B D

Proof

Step Hyp Ref Expression
1 declt.a
 |-  A e. NN0
2 declt.b
 |-  B e. NN0
3 declth.c
 |-  C e. NN0
4 declth.d
 |-  D e. NN0
5 declth.e
 |-  C <_ 9
6 declth.l
 |-  A < B
7 3 5 le9lt10
 |-  C < ; 1 0
8 1 2 3 4 7 6 decltc
 |-  ; A C < ; B D