Theorem dpval3rp

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

	Ref	Expression
Hypotheses	dpval3rp.a	$$⊢A\in {\mathbb{N}}_0$$
	dpval3rp.b	$$⊢B\in {ℝ}^{+}$$
Assertion	dpval3rp	Could not format assertion : No typesetting found for |- ( A . B ) = _ A B with typecode |-

Proof

Step	Hyp	Ref	Expression
1		dpval3rp.a	$$⊢A\in {\mathbb{N}}_0$$
2		dpval3rp.b	$$⊢B\in {ℝ}^{+}$$
3		rpre	$$⊢B\in {ℝ}^{+}\to B\in ℝ$$
4	2 3	ax-mp	$$⊢B\in ℝ$$
5	1 4	dpval3	Could not format ( A . B ) = _ A B : No typesetting found for |- ( A . B ) = _ A B with typecode |-