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 |
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 |