Metamath Proof Explorer


Theorem dp2ltsuc

Description: Comparing a decimal fraction with the next integer. (Contributed by Thierry Arnoux, 25-Dec-2021)

Ref Expression
Hypotheses dp2lt.a
|- A e. NN0
dp2lt.b
|- B e. RR+
dp2ltsuc.1
|- B < ; 1 0
dp2ltsuc.2
|- ( A + 1 ) = C
Assertion dp2ltsuc
|- _ A B < C

Proof

Step Hyp Ref Expression
1 dp2lt.a
 |-  A e. NN0
2 dp2lt.b
 |-  B e. RR+
3 dp2ltsuc.1
 |-  B < ; 1 0
4 dp2ltsuc.2
 |-  ( A + 1 ) = C
5 rpre
 |-  ( B e. RR+ -> B e. RR )
6 2 5 ax-mp
 |-  B e. RR
7 10re
 |-  ; 1 0 e. RR
8 10pos
 |-  0 < ; 1 0
9 6 7 7 8 ltdiv1ii
 |-  ( B < ; 1 0 <-> ( B / ; 1 0 ) < ( ; 1 0 / ; 1 0 ) )
10 3 9 mpbi
 |-  ( B / ; 1 0 ) < ( ; 1 0 / ; 1 0 )
11 7 recni
 |-  ; 1 0 e. CC
12 10nn
 |-  ; 1 0 e. NN
13 12 nnne0i
 |-  ; 1 0 =/= 0
14 11 13 dividi
 |-  ( ; 1 0 / ; 1 0 ) = 1
15 10 14 breqtri
 |-  ( B / ; 1 0 ) < 1
16 6 7 13 redivcli
 |-  ( B / ; 1 0 ) e. RR
17 1re
 |-  1 e. RR
18 1 nn0rei
 |-  A e. RR
19 16 17 18 ltadd2i
 |-  ( ( B / ; 1 0 ) < 1 <-> ( A + ( B / ; 1 0 ) ) < ( A + 1 ) )
20 15 19 mpbi
 |-  ( A + ( B / ; 1 0 ) ) < ( A + 1 )
21 df-dp2
 |-  _ A B = ( A + ( B / ; 1 0 ) )
22 4 eqcomi
 |-  C = ( A + 1 )
23 20 21 22 3brtr4i
 |-  _ A B < C