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 ⊢ A ∈ ℕ 0
rpdpcl.b ⊢ B ∈ ℝ +
Assertion rpdpcl ⊢ A . B ∈ ℝ +

Proof

Step Hyp Ref Expression
1 rpdpcl.a ⊢ A ∈ ℕ 0
2 rpdpcl.b ⊢ B ∈ ℝ +
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 ∈ ℝ +