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	⊢ 𝐴 ∈ ℕ0
	rpdpcl.b	⊢ 𝐵 ∈ ℝ+
Assertion	rpdpcl	⊢ ( 𝐴 . 𝐵 ) ∈ ℝ+

Proof

Step	Hyp	Ref	Expression
1		rpdpcl.a	⊢ 𝐴 ∈ ℕ0
2		rpdpcl.b	⊢ 𝐵 ∈ ℝ+
3	1 2	dpval3rp	⊢ ( 𝐴 . 𝐵 ) = _ 𝐴 𝐵
4	1 2	rpdp2cl	⊢ _ 𝐴 𝐵 ∈ ℝ+
5	3 4	eqeltri	⊢ ( 𝐴 . 𝐵 ) ∈ ℝ+