Theorem xnegcl

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

	Ref	Expression
Assertion	xnegcl	$$⊢A\in {ℝ}^{*}\to -A\in {ℝ}^{*}$$

Proof

Step	Hyp	Ref	Expression
1		elxr	$$⊢A\in {ℝ}^{*}\leftrightarrow \left(A\in ℝ\vee A=\mathrm{+\infty }\vee A=\mathrm{-\infty }\right)$$
2		rexneg	$$⊢A\in ℝ\to -A=-A$$
3		renegcl	$$⊢A\in ℝ\to -A\in ℝ$$
4	2 3	eqeltrd	$$⊢A\in ℝ\to -A\in ℝ$$
5	4	rexrd	$$⊢A\in ℝ\to -A\in {ℝ}^{*}$$
6		xnegeq	$$⊢A=\mathrm{+\infty }\to -A=-\mathrm{+\infty }$$
7		xnegpnf	$$⊢-\mathrm{+\infty }=\mathrm{-\infty }$$
8		mnfxr	$$⊢\mathrm{-\infty }\in {ℝ}^{*}$$
9	7 8	eqeltri	$$⊢-\mathrm{+\infty }\in {ℝ}^{*}$$
10	6 9	eqeltrdi	$$⊢A=\mathrm{+\infty }\to -A\in {ℝ}^{*}$$
11		xnegeq	$$⊢A=\mathrm{-\infty }\to -A=-\mathrm{-\infty }$$
12		xnegmnf	$$⊢-\mathrm{-\infty }=\mathrm{+\infty }$$
13		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
14	12 13	eqeltri	$$⊢-\mathrm{-\infty }\in {ℝ}^{*}$$
15	11 14	eqeltrdi	$$⊢A=\mathrm{-\infty }\to -A\in {ℝ}^{*}$$
16	5 10 15	3jaoi	$$⊢\left(A\in ℝ\vee A=\mathrm{+\infty }\vee A=\mathrm{-\infty }\right)\to -A\in {ℝ}^{*}$$
17	1 16	sylbi	$$⊢A\in {ℝ}^{*}\to -A\in {ℝ}^{*}$$