Metamath Proof Explorer


Theorem dpcl

Description: Prove that the closure of the decimal point is RR as we have defined it. See df-dp . (Contributed by David A. Wheeler, 15-May-2015)

Ref Expression
Assertion dpcl ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℝ ) → ( 𝐴 . 𝐵 ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 dpval ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℝ ) → ( 𝐴 . 𝐵 ) = 𝐴 𝐵 )
2 nn0re ( 𝐴 ∈ ℕ0𝐴 ∈ ℝ )
3 dp2cl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 𝐵 ∈ ℝ )
4 2 3 sylan ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℝ ) → 𝐴 𝐵 ∈ ℝ )
5 1 4 eqeltrd ( ( 𝐴 ∈ ℕ0𝐵 ∈ ℝ ) → ( 𝐴 . 𝐵 ) ∈ ℝ )