Metamath Proof Explorer

Theorem dp2lt

Description: Comparing two decimal fractions (equal unit places). (Contributed by Thierry Arnoux, 16-Dec-2021)

Ref Expression
Hypotheses dp2lt.a 
|- A e. NN0
dp2lt.b 
|- B e. RR+
dp2lt.c 
|- C e. RR+
dp2lt.l 
|- B < C
Assertion dp2lt 
|- _ A B < _ A C

Proof

Step Hyp Ref Expression
1 dp2lt.a 
 |-  A e. NN0
2 dp2lt.b 
 |-  B e. RR+
3 dp2lt.c 
 |-  C e. RR+
4 dp2lt.l 
 |-  B < C
5 rpssre 
 |-  RR+ C_ RR
6 5 2 sselii 
 |-  B e. RR
7 10re 
 |-  ; 1 0 e. RR
8 0re 
 |-  0 e. RR
9 10pos 
 |-  0 < ; 1 0
10 8 9 gtneii 
 |-  ; 1 0 =/= 0
11 redivcl 
 |-  ( ( B e. RR /\ ; 1 0 e. RR /\ ; 1 0 =/= 0 ) -> ( B / ; 1 0 ) e. RR )
12 6 7 10 11 mp3an 
 |-  ( B / ; 1 0 ) e. RR
13 5 3 sselii 
 |-  C e. RR
14 redivcl 
 |-  ( ( C e. RR /\ ; 1 0 e. RR /\ ; 1 0 =/= 0 ) -> ( C / ; 1 0 ) e. RR )
15 13 7 10 14 mp3an 
 |-  ( C / ; 1 0 ) e. RR
16 1 nn0rei 
 |-  A e. RR
17 12 15 16 3pm3.2i 
 |-  ( ( B / ; 1 0 ) e. RR /\ ( C / ; 1 0 ) e. RR /\ A e. RR )
18 7 9 pm3.2i 
 |-  ( ; 1 0 e. RR /\ 0 < ; 1 0 )
19 ltdiv1 
 |-  ( ( B e. RR /\ C e. RR /\ ( ; 1 0 e. RR /\ 0 < ; 1 0 ) ) -> ( B < C <-> ( B / ; 1 0 ) < ( C / ; 1 0 ) ) )
20 6 13 18 19 mp3an 
 |-  ( B < C <-> ( B / ; 1 0 ) < ( C / ; 1 0 ) )
21 4 20 mpbi 
 |-  ( B / ; 1 0 ) < ( C / ; 1 0 )
22 axltadd 
 |-  ( ( ( B / ; 1 0 ) e. RR /\ ( C / ; 1 0 ) e. RR /\ A e. RR ) -> ( ( B / ; 1 0 ) < ( C / ; 1 0 ) -> ( A + ( B / ; 1 0 ) ) < ( A + ( C / ; 1 0 ) ) ) )
23 22 imp 
 |-  ( ( ( ( B / ; 1 0 ) e. RR /\ ( C / ; 1 0 ) e. RR /\ A e. RR ) /\ ( B / ; 1 0 ) < ( C / ; 1 0 ) ) -> ( A + ( B / ; 1 0 ) ) < ( A + ( C / ; 1 0 ) ) )
24 17 21 23 mp2an 
 |-  ( A + ( B / ; 1 0 ) ) < ( A + ( C / ; 1 0 ) )
25 df-dp2 
 |-  _ A B = ( A + ( B / ; 1 0 ) )
26 df-dp2 
 |-  _ A C = ( A + ( C / ; 1 0 ) )
27 24 25 26 3brtr4i 
 |-  _ A B < _ A C