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

Metamath Proof Explorer

Theorem rpdpcl

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

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

Proof

Step Hyp Ref Expression
1 rpdpcl.a 
 |-  A e. NN0
2 rpdpcl.b 
 |-  B e. RR+
3 1 2 dpval3rp 
 |-  ( A . B ) = _ A B
4 1 2 rpdp2cl 
 |-  _ A B e. RR+
5 3 4 eqeltri 
 |-  ( A . B ) e. RR+