Theorem xmulcld

Description: Closure of extended real multiplication. (Contributed by Mario Carneiro, 28-May-2016)

	Ref	Expression
Hypotheses	xnegcld.1	$$⊢\phi \to A\in {ℝ}^{*}$$
	xaddcld.2	$$⊢\phi \to B\in {ℝ}^{*}$$
Assertion	xmulcld	$$⊢\phi \to A{\cdot }_{𝑒}B\in {ℝ}^{*}$$

Proof

Step	Hyp	Ref	Expression
1		xnegcld.1	$$⊢\phi \to A\in {ℝ}^{*}$$
2		xaddcld.2	$$⊢\phi \to B\in {ℝ}^{*}$$
3		xmulcl	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to A{\cdot }_{𝑒}B\in {ℝ}^{*}$$
4	1 2 3	syl2anc	$$⊢\phi \to A{\cdot }_{𝑒}B\in {ℝ}^{*}$$