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