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 𝐴 ∈ ℕ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 ( 𝐴 . 𝐵 ) ∈ ℝ+