This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dpval3rp

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

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

Step	Hyp	Ref	Expression
1		dpval3rp.a	$⊢ A \in ℕ_{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 \|-