Metamath Proof Explorer

Theorem dp2ltc

Description: Comparing two decimal expansions (unequal higher places). (Contributed by Thierry Arnoux, 16-Dec-2021)

Ref Expression
Hypotheses dp2lt.a 
|- A e. NN0
dp2lt.b 
|- B e. RR+
dp2ltc.c 
|- C e. NN0
dp2ltc.d 
|- D e. RR+
dp2ltc.s 
|- B < ; 1 0
dp2ltc.l 
|- A < C
Assertion dp2ltc 
|- _ A B < _ C D

Proof

Step Hyp Ref Expression
1 dp2lt.a 
 |-  A e. NN0
2 dp2lt.b 
 |-  B e. RR+
3 dp2ltc.c 
 |-  C e. NN0
4 dp2ltc.d 
 |-  D e. RR+
5 dp2ltc.s 
 |-  B < ; 1 0
6 dp2ltc.l 
 |-  A < C
7 rpssre 
 |-  RR+ C_ RR
8 7 2 sselii 
 |-  B e. RR
9 10re 
 |-  ; 1 0 e. RR
10 10pos 
 |-  0 < ; 1 0
11 elrp 
 |-  ( ; 1 0 e. RR+ <-> ( ; 1 0 e. RR /\ 0 < ; 1 0 ) )
12 9 10 11 mpbir2an 
 |-  ; 1 0 e. RR+
13 divlt1lt 
 |-  ( ( B e. RR /\ ; 1 0 e. RR+ ) -> ( ( B / ; 1 0 ) < 1 <-> B < ; 1 0 ) )
14 8 12 13 mp2an 
 |-  ( ( B / ; 1 0 ) < 1 <-> B < ; 1 0 )
15 5 14 mpbir 
 |-  ( B / ; 1 0 ) < 1
16 9 10 gt0ne0ii 
 |-  ; 1 0 =/= 0
17 8 9 16 redivcli 
 |-  ( B / ; 1 0 ) e. RR
18 1re 
 |-  1 e. RR
19 1 nn0rei 
 |-  A e. RR
20 ltadd2 
 |-  ( ( ( B / ; 1 0 ) e. RR /\ 1 e. RR /\ A e. RR ) -> ( ( B / ; 1 0 ) < 1 <-> ( A + ( B / ; 1 0 ) ) < ( A + 1 ) ) )
21 17 18 19 20 mp3an 
 |-  ( ( B / ; 1 0 ) < 1 <-> ( A + ( B / ; 1 0 ) ) < ( A + 1 ) )
22 15 21 mpbi 
 |-  ( A + ( B / ; 1 0 ) ) < ( A + 1 )
23 1 nn0zi 
 |-  A e. ZZ
24 3 nn0zi 
 |-  C e. ZZ
25 zltp1le 
 |-  ( ( A e. ZZ /\ C e. ZZ ) -> ( A < C <-> ( A + 1 ) <_ C ) )
26 23 24 25 mp2an 
 |-  ( A < C <-> ( A + 1 ) <_ C )
27 6 26 mpbi 
 |-  ( A + 1 ) <_ C
28 19 17 readdcli 
 |-  ( A + ( B / ; 1 0 ) ) e. RR
29 19 18 readdcli 
 |-  ( A + 1 ) e. RR
30 3 nn0rei 
 |-  C e. RR
31 28 29 30 ltletri 
 |-  ( ( ( A + ( B / ; 1 0 ) ) < ( A + 1 ) /\ ( A + 1 ) <_ C ) -> ( A + ( B / ; 1 0 ) ) < C )
32 22 27 31 mp2an 
 |-  ( A + ( B / ; 1 0 ) ) < C
33 4 12 pm3.2i 
 |-  ( D e. RR+ /\ ; 1 0 e. RR+ )
34 rpdivcl 
 |-  ( ( D e. RR+ /\ ; 1 0 e. RR+ ) -> ( D / ; 1 0 ) e. RR+ )
35 33 34 ax-mp 
 |-  ( D / ; 1 0 ) e. RR+
36 ltaddrp 
 |-  ( ( C e. RR /\ ( D / ; 1 0 ) e. RR+ ) -> C < ( C + ( D / ; 1 0 ) ) )
37 30 35 36 mp2an 
 |-  C < ( C + ( D / ; 1 0 ) )
38 7 4 sselii 
 |-  D e. RR
39 38 9 16 redivcli 
 |-  ( D / ; 1 0 ) e. RR
40 30 39 readdcli 
 |-  ( C + ( D / ; 1 0 ) ) e. RR
41 28 30 40 lttri 
 |-  ( ( ( A + ( B / ; 1 0 ) ) < C /\ C < ( C + ( D / ; 1 0 ) ) ) -> ( A + ( B / ; 1 0 ) ) < ( C + ( D / ; 1 0 ) ) )
42 32 37 41 mp2an 
 |-  ( A + ( B / ; 1 0 ) ) < ( C + ( D / ; 1 0 ) )
43 df-dp2 
 |-  _ A B = ( A + ( B / ; 1 0 ) )
44 df-dp2 
 |-  _ C D = ( C + ( D / ; 1 0 ) )
45 42 43 44 3brtr4i 
 |-  _ A B < _ C D