Theorem xaddcld

Description: The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 28-May-2016)

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

Proof

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