Metamath Proof Explorer

Theorem dpgti

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

Ref Expression
Hypotheses dpgti.a 
|- A e. NN0
dpgti.b 
|- B e. RR+
Assertion dpgti 
|- A < ( A . B )

Proof

Step Hyp Ref Expression
1 dpgti.a 
 |-  A e. NN0
2 dpgti.b 
 |-  B e. RR+
3 1 nn0rei 
 |-  A e. RR
4 10re 
 |-  ; 1 0 e. RR
5 10pos 
 |-  0 < ; 1 0
6 4 5 pm3.2i 
 |-  ( ; 1 0 e. RR /\ 0 < ; 1 0 )
7 elrp 
 |-  ( ; 1 0 e. RR+ <-> ( ; 1 0 e. RR /\ 0 < ; 1 0 ) )
8 6 7 mpbir 
 |-  ; 1 0 e. RR+
9 rpdivcl 
 |-  ( ( B e. RR+ /\ ; 1 0 e. RR+ ) -> ( B / ; 1 0 ) e. RR+ )
10 2 8 9 mp2an 
 |-  ( B / ; 1 0 ) e. RR+
11 ltaddrp 
 |-  ( ( A e. RR /\ ( B / ; 1 0 ) e. RR+ ) -> A < ( A + ( B / ; 1 0 ) ) )
12 3 10 11 mp2an 
 |-  A < ( A + ( B / ; 1 0 ) )
13 rpre 
 |-  ( B e. RR+ -> B e. RR )
14 2 13 ax-mp 
 |-  B e. RR
15 1 14 dpval2 
 |-  ( A . B ) = ( A + ( B / ; 1 0 ) )
16 12 15 breqtrri 
 |-  A < ( A . B )