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

Metamath Proof Explorer

Theorem xmulcl

Description: Closure of extended real multiplication. (Contributed by Mario Carneiro, 20-Aug-2015)

		Ref	Expression
	Assertion	xmulcl	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to A \cdot_{𝑒} B \in ℝ^{*}$

Step	Hyp	Ref	Expression
1		xmulf	$⊢ \cdot_{𝑒} : ℝ^{} \times ℝ^{} ⟶ ℝ^{*}$
2	1	fovcl	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to A \cdot_{𝑒} B \in ℝ^{*}$