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