Theorem dpval3rp

Description: Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021)

	Ref	Expression
Hypotheses	dpval3rp.a	⊢ 𝐴 ∈ ℕ0
	dpval3rp.b	⊢ 𝐵 ∈ ℝ+
Assertion	dpval3rp	⊢ ( 𝐴 . 𝐵 ) = _ 𝐴 𝐵

Proof

Step	Hyp	Ref	Expression
1		dpval3rp.a	⊢ 𝐴 ∈ ℕ0
2		dpval3rp.b	⊢ 𝐵 ∈ ℝ+
3		rpre	⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ∈ ℝ )
4	2 3	ax-mp	⊢ 𝐵 ∈ ℝ
5	1 4	dpval3	⊢ ( 𝐴 . 𝐵 ) = _ 𝐴 𝐵