Metamath Proof Explorer


Theorem decle

Description: Comparing two decimal integers (equal 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
decle.4
|- B <_ C
Assertion decle
|- ; A B <_ ; A C

Proof

Step Hyp Ref Expression
1 decle.1
 |-  A e. NN0
2 decle.2
 |-  B e. NN0
3 decle.3
 |-  C e. NN0
4 decle.4
 |-  B <_ C
5 2 nn0rei
 |-  B e. RR
6 3 nn0rei
 |-  C e. RR
7 10nn0
 |-  ; 1 0 e. NN0
8 7 1 nn0mulcli
 |-  ( ; 1 0 x. A ) e. NN0
9 8 nn0rei
 |-  ( ; 1 0 x. A ) e. RR
10 5 6 9 leadd2i
 |-  ( B <_ C <-> ( ( ; 1 0 x. A ) + B ) <_ ( ( ; 1 0 x. A ) + C ) )
11 4 10 mpbi
 |-  ( ( ; 1 0 x. A ) + B ) <_ ( ( ; 1 0 x. A ) + C )
12 dfdec10
 |-  ; A B = ( ( ; 1 0 x. A ) + B )
13 dfdec10
 |-  ; A C = ( ( ; 1 0 x. A ) + C )
14 11 12 13 3brtr4i
 |-  ; A B <_ ; A C