Theorem xnegid

Description: Extended real version of negid . (Contributed by Mario Carneiro, 20-Aug-2015)

	Ref	Expression
Assertion	xnegid	$$⊢A\in {ℝ}^{*}\to A{+}_{𝑒}\left(-A\right)=0$$

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	2	oveq2d	$$⊢A\in ℝ\to A{+}_{𝑒}\left(-A\right)=A{+}_{𝑒}\left(-A\right)$$
4		renegcl	$$⊢A\in ℝ\to -A\in ℝ$$
5		rexadd	$$⊢\left(A\in ℝ\wedge -A\in ℝ\right)\to A{+}_{𝑒}\left(-A\right)=A+\left(-A\right)$$
6	4 5	mpdan	$$⊢A\in ℝ\to A{+}_{𝑒}\left(-A\right)=A+\left(-A\right)$$
7		recn	$$⊢A\in ℝ\to A\in ℂ$$
8	7	negidd	$$⊢A\in ℝ\to A+\left(-A\right)=0$$
9	3 6 8	3eqtrd	$$⊢A\in ℝ\to A{+}_{𝑒}\left(-A\right)=0$$
10		id	$$⊢A=\mathrm{+\infty }\to A=\mathrm{+\infty }$$
11		xnegeq	$$⊢A=\mathrm{+\infty }\to -A=-\mathrm{+\infty }$$
12		xnegpnf	$$⊢-\mathrm{+\infty }=\mathrm{-\infty }$$
13	11 12	eqtrdi	$$⊢A=\mathrm{+\infty }\to -A=\mathrm{-\infty }$$
14	10 13	oveq12d	$$⊢A=\mathrm{+\infty }\to A{+}_{𝑒}\left(-A\right)=\mathrm{+\infty }{+}_{𝑒}\mathrm{-\infty }$$
15		pnfaddmnf	$$⊢\mathrm{+\infty }{+}_{𝑒}\mathrm{-\infty }=0$$
16	14 15	eqtrdi	$$⊢A=\mathrm{+\infty }\to A{+}_{𝑒}\left(-A\right)=0$$
17		id	$$⊢A=\mathrm{-\infty }\to A=\mathrm{-\infty }$$
18		xnegeq	$$⊢A=\mathrm{-\infty }\to -A=-\mathrm{-\infty }$$
19		xnegmnf	$$⊢-\mathrm{-\infty }=\mathrm{+\infty }$$
20	18 19	eqtrdi	$$⊢A=\mathrm{-\infty }\to -A=\mathrm{+\infty }$$
21	17 20	oveq12d	$$⊢A=\mathrm{-\infty }\to A{+}_{𝑒}\left(-A\right)=\mathrm{-\infty }{+}_{𝑒}\mathrm{+\infty }$$
22		mnfaddpnf	$$⊢\mathrm{-\infty }{+}_{𝑒}\mathrm{+\infty }=0$$
23	21 22	eqtrdi	$$⊢A=\mathrm{-\infty }\to A{+}_{𝑒}\left(-A\right)=0$$
24	9 16 23	3jaoi	$$⊢\left(A\in ℝ\vee A=\mathrm{+\infty }\vee A=\mathrm{-\infty }\right)\to A{+}_{𝑒}\left(-A\right)=0$$
25	1 24	sylbi	$$⊢A\in {ℝ}^{*}\to A{+}_{𝑒}\left(-A\right)=0$$