Metamath Proof Explorer

Theorem dp2lt10

Description: Decimal fraction builds real numbers less than 10. (Contributed by Thierry Arnoux, 16-Dec-2021)

Ref Expression
Hypotheses dp2lt10.a 
|- A e. NN0
dp2lt10.b 
|- B e. RR+
dp2lt10.1 
|- A < ; 1 0
dp2lt10.2 
|- B < ; 1 0
Assertion dp2lt10 
|- _ A B < ; 1 0

Proof

Step Hyp Ref Expression
1 dp2lt10.a 
 |-  A e. NN0
2 dp2lt10.b 
 |-  B e. RR+
3 dp2lt10.1 
 |-  A < ; 1 0
4 dp2lt10.2 
 |-  B < ; 1 0
5 df-dp2 
 |-  _ A B = ( A + ( B / ; 1 0 ) )
6 9p1e10 
 |-  ( 9 + 1 ) = ; 1 0
7 3 6 breqtrri 
 |-  A < ( 9 + 1 )
8 1 nn0zi 
 |-  A e. ZZ
9 9nn0 
 |-  9 e. NN0
10 9 nn0zi 
 |-  9 e. ZZ
11 zleltp1 
 |-  ( ( A e. ZZ /\ 9 e. ZZ ) -> ( A <_ 9 <-> A < ( 9 + 1 ) ) )
12 8 10 11 mp2an 
 |-  ( A <_ 9 <-> A < ( 9 + 1 ) )
13 7 12 mpbir 
 |-  A <_ 9
14 rpssre 
 |-  RR+ C_ RR
15 14 2 sselii 
 |-  B e. RR
16 10re 
 |-  ; 1 0 e. RR
17 10pos 
 |-  0 < ; 1 0
18 16 17 elrpii 
 |-  ; 1 0 e. RR+
19 divlt1lt 
 |-  ( ( B e. RR /\ ; 1 0 e. RR+ ) -> ( ( B / ; 1 0 ) < 1 <-> B < ; 1 0 ) )
20 15 18 19 mp2an 
 |-  ( ( B / ; 1 0 ) < 1 <-> B < ; 1 0 )
21 4 20 mpbir 
 |-  ( B / ; 1 0 ) < 1
22 1 nn0rei 
 |-  A e. RR
23 0re 
 |-  0 e. RR
24 23 17 gtneii 
 |-  ; 1 0 =/= 0
25 15 16 24 redivcli 
 |-  ( B / ; 1 0 ) e. RR
26 22 25 pm3.2i 
 |-  ( A e. RR /\ ( B / ; 1 0 ) e. RR )
27 9re 
 |-  9 e. RR
28 1re 
 |-  1 e. RR
29 27 28 pm3.2i 
 |-  ( 9 e. RR /\ 1 e. RR )
30 leltadd 
 |-  ( ( ( A e. RR /\ ( B / ; 1 0 ) e. RR ) /\ ( 9 e. RR /\ 1 e. RR ) ) -> ( ( A <_ 9 /\ ( B / ; 1 0 ) < 1 ) -> ( A + ( B / ; 1 0 ) ) < ( 9 + 1 ) ) )
31 26 29 30 mp2an 
 |-  ( ( A <_ 9 /\ ( B / ; 1 0 ) < 1 ) -> ( A + ( B / ; 1 0 ) ) < ( 9 + 1 ) )
32 13 21 31 mp2an 
 |-  ( A + ( B / ; 1 0 ) ) < ( 9 + 1 )
33 32 6 breqtri 
 |-  ( A + ( B / ; 1 0 ) ) < ; 1 0
34 5 33 eqbrtri 
 |-  _ A B < ; 1 0