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+