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\in {\mathbb{N}}_0$$
	rpdpcl.b	$$⊢B\in {ℝ}^{+}$$
Assertion	rpdpcl	$$⊢A.B\in {ℝ}^{+}$$

Proof

Step	Hyp	Ref	Expression
1		rpdpcl.a	$$⊢A\in {\mathbb{N}}_0$$
2		rpdpcl.b	$$⊢B\in {ℝ}^{+}$$
3	1 2	dpval3rp	Could not format ( A . B ) = _ A B : No typesetting found for |- ( A . B ) = _ A B with typecode |-
4	1 2	rpdp2cl	Could not format _ A B e. RR+ : No typesetting found for |- _ A B e. RR+ with typecode |-
5	3 4	eqeltri	$$⊢A.B\in {ℝ}^{+}$$