This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rpdp2cl

Description: Closure for a decimal fraction in the positive real numbers. (Contributed by Thierry Arnoux, 16-Dec-2021)

Ref Expression
Hypotheses rpdp2cl.a 
|- A e. NN0
rpdp2cl.b 
|- B e. RR+
Assertion rpdp2cl 
|- _ A B e. RR+

Proof

Step Hyp Ref Expression
1 rpdp2cl.a 
 |-  A e. NN0
2 rpdp2cl.b 
 |-  B e. RR+
3 df-dp2 
 |-  _ A B = ( A + ( B / ; 1 0 ) )
4 1 nn0rei 
 |-  A e. RR
5 rpssre 
 |-  RR+ C_ RR
6 10nn 
 |-  ; 1 0 e. NN
7 nnrp 
 |-  ( ; 1 0 e. NN -> ; 1 0 e. RR+ )
8 6 7 ax-mp 
 |-  ; 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 5 10 sselii 
 |-  ( B / ; 1 0 ) e. RR
12 readdcl 
 |-  ( ( A e. RR /\ ( B / ; 1 0 ) e. RR ) -> ( A + ( B / ; 1 0 ) ) e. RR )
13 4 11 12 mp2an 
 |-  ( A + ( B / ; 1 0 ) ) e. RR
14 4 11 pm3.2i 
 |-  ( A e. RR /\ ( B / ; 1 0 ) e. RR )
15 1 nn0ge0i 
 |-  0 <_ A
16 rpgt0 
 |-  ( ( B / ; 1 0 ) e. RR+ -> 0 < ( B / ; 1 0 ) )
17 10 16 ax-mp 
 |-  0 < ( B / ; 1 0 )
18 15 17 pm3.2i 
 |-  ( 0 <_ A /\ 0 < ( B / ; 1 0 ) )
19 addgegt0 
 |-  ( ( ( A e. RR /\ ( B / ; 1 0 ) e. RR ) /\ ( 0 <_ A /\ 0 < ( B / ; 1 0 ) ) ) -> 0 < ( A + ( B / ; 1 0 ) ) )
20 14 18 19 mp2an 
 |-  0 < ( A + ( B / ; 1 0 ) )
21 elrp 
 |-  ( ( A + ( B / ; 1 0 ) ) e. RR+ <-> ( ( A + ( B / ; 1 0 ) ) e. RR /\ 0 < ( A + ( B / ; 1 0 ) ) ) )
22 13 20 21 mpbir2an 
 |-  ( A + ( B / ; 1 0 ) ) e. RR+
23 3 22 eqeltri 
 |-  _ A B e. RR+