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 A0
dp2lt.b B+
dp2lt.c C+
dp2lt.l B<C
Assertion dp2lt Could not format assertion : No typesetting found for |- _ A B < _ A C with typecode |-

Proof

Step Hyp Ref Expression
1 dp2lt.a A0
2 dp2lt.b B+
3 dp2lt.c C+
4 dp2lt.l B<C
5 rpssre +
6 5 2 sselii B
7 10re 10
8 0re 0
9 10pos 0<10
10 8 9 gtneii 100
11 redivcl B10100B10
12 6 7 10 11 mp3an B10
13 5 3 sselii C
14 redivcl C10100C10
15 13 7 10 14 mp3an C10
16 1 nn0rei A
17 12 15 16 3pm3.2i B10C10A
18 7 9 pm3.2i 100<10
19 ltdiv1 BC100<10B<CB10<C10
20 6 13 18 19 mp3an B<CB10<C10
21 4 20 mpbi B10<C10
22 axltadd B10C10AB10<C10A+B10<A+C10
23 22 imp B10C10AB10<C10A+B10<A+C10
24 17 21 23 mp2an A+B10<A+C10
25 df-dp2 Could not format _ A B = ( A + ( B / ; 1 0 ) ) : No typesetting found for |- _ A B = ( A + ( B / ; 1 0 ) ) with typecode |-
26 df-dp2 Could not format _ A C = ( A + ( C / ; 1 0 ) ) : No typesetting found for |- _ A C = ( A + ( C / ; 1 0 ) ) with typecode |-
27 24 25 26 3brtr4i Could not format _ A B < _ A C : No typesetting found for |- _ A B < _ A C with typecode |-