Metamath Proof Explorer


Theorem decleh

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

Ref Expression
Hypotheses decle.1
|- A e. NN0
decle.2
|- B e. NN0
decle.3
|- C e. NN0
decleh.4
|- D e. NN0
decleh.5
|- C <_ 9
decleh.6
|- A < B
Assertion decleh
|- ; A C <_ ; B D

Proof

Step Hyp Ref Expression
1 decle.1
 |-  A e. NN0
2 decle.2
 |-  B e. NN0
3 decle.3
 |-  C e. NN0
4 decleh.4
 |-  D e. NN0
5 decleh.5
 |-  C <_ 9
6 decleh.6
 |-  A < B
7 1 3 deccl
 |-  ; A C e. NN0
8 7 nn0rei
 |-  ; A C e. RR
9 2 4 deccl
 |-  ; B D e. NN0
10 9 nn0rei
 |-  ; B D e. RR
11 1 2 3 4 5 6 declth
 |-  ; A C < ; B D
12 8 10 11 ltleii
 |-  ; A C <_ ; B D