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