Theorem xrge0addcld

Description: Nonnegative extended reals are closed under addition. (Contributed by Thierry Arnoux, 16-Sep-2019)

	Ref	Expression
Hypotheses	xrge0addcld.a	$$⊢\phi \to A\in \left[0,\mathrm{+\infty }\right]$$
	xrge0addcld.b	$$⊢\phi \to B\in \left[0,\mathrm{+\infty }\right]$$
Assertion	xrge0addcld	$$⊢\phi \to A{+}_{𝑒}B\in \left[0,\mathrm{+\infty }\right]$$

Proof

Step	Hyp	Ref	Expression
1		xrge0addcld.a	$$⊢\phi \to A\in \left[0,\mathrm{+\infty }\right]$$
2		xrge0addcld.b	$$⊢\phi \to B\in \left[0,\mathrm{+\infty }\right]$$
3		elxrge0	$$⊢A\in \left[0,\mathrm{+\infty }\right]\leftrightarrow \left(A\in {ℝ}^{*}\wedge 0\le A\right)$$
4	1 3	sylib	$$⊢\phi \to \left(A\in {ℝ}^{*}\wedge 0\le A\right)$$
5	4	simpld	$$⊢\phi \to A\in {ℝ}^{*}$$
6		elxrge0	$$⊢B\in \left[0,\mathrm{+\infty }\right]\leftrightarrow \left(B\in {ℝ}^{*}\wedge 0\le B\right)$$
7	2 6	sylib	$$⊢\phi \to \left(B\in {ℝ}^{*}\wedge 0\le B\right)$$
8	7	simpld	$$⊢\phi \to B\in {ℝ}^{*}$$
9	5 8	xaddcld	$$⊢\phi \to A{+}_{𝑒}B\in {ℝ}^{*}$$
10	4	simprd	$$⊢\phi \to 0\le A$$
11	7	simprd	$$⊢\phi \to 0\le B$$
12		xaddge0	$$⊢\left(\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\wedge \left(0\le A\wedge 0\le B\right)\right)\to 0\le A{+}_{𝑒}B$$
13	5 8 10 11 12	syl22anc	$$⊢\phi \to 0\le A{+}_{𝑒}B$$
14		elxrge0	$$⊢A{+}_{𝑒}B\in \left[0,\mathrm{+\infty }\right]\leftrightarrow \left(A{+}_{𝑒}B\in {ℝ}^{*}\wedge 0\le A{+}_{𝑒}B\right)$$
15	9 13 14	sylanbrc	$$⊢\phi \to A{+}_{𝑒}B\in \left[0,\mathrm{+\infty }\right]$$