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