Metamath Proof Explorer

Theorem dplti

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

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

Proof

Step Hyp Ref Expression
1 dplti.a 
 |-  A e. NN0
2 dplti.b 
 |-  B e. RR+
3 dplti.c 
 |-  C e. NN0
4 dplti.1 
 |-  B < ; 1 0
5 dplti.2 
 |-  ( A + 1 ) = C
6 rpre 
 |-  ( B e. RR+ -> B e. RR )
7 2 6 ax-mp 
 |-  B e. RR
8 1 7 dpval2 
 |-  ( A . B ) = ( A + ( B / ; 1 0 ) )
9 10re 
 |-  ; 1 0 e. RR
10 10pos 
 |-  0 < ; 1 0
11 9 10 pm3.2i 
 |-  ( ; 1 0 e. RR /\ 0 < ; 1 0 )
12 elrp 
 |-  ( ; 1 0 e. RR+ <-> ( ; 1 0 e. RR /\ 0 < ; 1 0 ) )
13 11 12 mpbir 
 |-  ; 1 0 e. RR+
14 divlt1lt 
 |-  ( ( B e. RR /\ ; 1 0 e. RR+ ) -> ( ( B / ; 1 0 ) < 1 <-> B < ; 1 0 ) )
15 7 13 14 mp2an 
 |-  ( ( B / ; 1 0 ) < 1 <-> B < ; 1 0 )
16 4 15 mpbir 
 |-  ( B / ; 1 0 ) < 1
17 0re 
 |-  0 e. RR
18 17 10 gtneii 
 |-  ; 1 0 =/= 0
19 7 9 18 redivcli 
 |-  ( B / ; 1 0 ) e. RR
20 1re 
 |-  1 e. RR
21 nn0ssre 
 |-  NN0 C_ RR
22 21 1 sselii 
 |-  A e. RR
23 19 20 22 ltadd2i 
 |-  ( ( B / ; 1 0 ) < 1 <-> ( A + ( B / ; 1 0 ) ) < ( A + 1 ) )
24 16 23 mpbi 
 |-  ( A + ( B / ; 1 0 ) ) < ( A + 1 )
25 8 24 eqbrtri 
 |-  ( A . B ) < ( A + 1 )
26 25 5 breqtri 
 |-  ( A . B ) < C