Metamath Proof Explorer

Theorem numltc

Description: Comparing two decimal integers (unequal higher places). (Contributed by Mario Carneiro, 18-Feb-2014)

Ref Expression
Hypotheses numlt.1 
|- T e. NN
numlt.2 
|- A e. NN0
numlt.3 
|- B e. NN0
numltc.3 
|- C e. NN0
numltc.4 
|- D e. NN0
numltc.5 
|- C < T
numltc.6 
|- A < B
Assertion numltc 
|- ( ( T x. A ) + C ) < ( ( T x. B ) + D )

Proof

Step Hyp Ref Expression
1 numlt.1 
 |-  T e. NN
2 numlt.2 
 |-  A e. NN0
3 numlt.3 
 |-  B e. NN0
4 numltc.3 
 |-  C e. NN0
5 numltc.4 
 |-  D e. NN0
6 numltc.5 
 |-  C < T
7 numltc.6 
 |-  A < B
8 1 2 4 1 6 numlt 
 |-  ( ( T x. A ) + C ) < ( ( T x. A ) + T )
9 1 nnrei 
 |-  T e. RR
10 9 recni 
 |-  T e. CC
11 2 nn0rei 
 |-  A e. RR
12 11 recni 
 |-  A e. CC
13 ax-1cn 
 |-  1 e. CC
14 10 12 13 adddii 
 |-  ( T x. ( A + 1 ) ) = ( ( T x. A ) + ( T x. 1 ) )
15 10 mulid1i 
 |-  ( T x. 1 ) = T
16 15 oveq2i 
 |-  ( ( T x. A ) + ( T x. 1 ) ) = ( ( T x. A ) + T )
17 14 16 eqtri 
 |-  ( T x. ( A + 1 ) ) = ( ( T x. A ) + T )
18 8 17 breqtrri 
 |-  ( ( T x. A ) + C ) < ( T x. ( A + 1 ) )
19 nn0ltp1le 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( A < B <-> ( A + 1 ) <_ B ) )
20 2 3 19 mp2an 
 |-  ( A < B <-> ( A + 1 ) <_ B )
21 7 20 mpbi 
 |-  ( A + 1 ) <_ B
22 1 nngt0i 
 |-  0 < T
23 peano2re 
 |-  ( A e. RR -> ( A + 1 ) e. RR )
24 11 23 ax-mp 
 |-  ( A + 1 ) e. RR
25 3 nn0rei 
 |-  B e. RR
26 24 25 9 lemul2i 
 |-  ( 0 < T -> ( ( A + 1 ) <_ B <-> ( T x. ( A + 1 ) ) <_ ( T x. B ) ) )
27 22 26 ax-mp 
 |-  ( ( A + 1 ) <_ B <-> ( T x. ( A + 1 ) ) <_ ( T x. B ) )
28 21 27 mpbi 
 |-  ( T x. ( A + 1 ) ) <_ ( T x. B )
29 9 11 remulcli 
 |-  ( T x. A ) e. RR
30 4 nn0rei 
 |-  C e. RR
31 29 30 readdcli 
 |-  ( ( T x. A ) + C ) e. RR
32 9 24 remulcli 
 |-  ( T x. ( A + 1 ) ) e. RR
33 9 25 remulcli 
 |-  ( T x. B ) e. RR
34 31 32 33 ltletri 
 |-  ( ( ( ( T x. A ) + C ) < ( T x. ( A + 1 ) ) /\ ( T x. ( A + 1 ) ) <_ ( T x. B ) ) -> ( ( T x. A ) + C ) < ( T x. B ) )
35 18 28 34 mp2an 
 |-  ( ( T x. A ) + C ) < ( T x. B )
36 33 5 nn0addge1i 
 |-  ( T x. B ) <_ ( ( T x. B ) + D )
37 5 nn0rei 
 |-  D e. RR
38 33 37 readdcli 
 |-  ( ( T x. B ) + D ) e. RR
39 31 33 38 ltletri 
 |-  ( ( ( ( T x. A ) + C ) < ( T x. B ) /\ ( T x. B ) <_ ( ( T x. B ) + D ) ) -> ( ( T x. A ) + C ) < ( ( T x. B ) + D ) )
40 35 36 39 mp2an 
 |-  ( ( T x. A ) + C ) < ( ( T x. B ) + D )