Theorem xnegid

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

	Ref	Expression
Assertion	xnegid	⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 +𝑒 -𝑒 𝐴 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		elxr	⊢ ( 𝐴 ∈ ℝ* ↔ ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) )
2		rexneg	⊢ ( 𝐴 ∈ ℝ → -𝑒 𝐴 = - 𝐴 )
3	2	oveq2d	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 +𝑒 -𝑒 𝐴 ) = ( 𝐴 +𝑒 - 𝐴 ) )
4		renegcl	⊢ ( 𝐴 ∈ ℝ → - 𝐴 ∈ ℝ )
5		rexadd	⊢ ( ( 𝐴 ∈ ℝ ∧ - 𝐴 ∈ ℝ ) → ( 𝐴 +𝑒 - 𝐴 ) = ( 𝐴 + - 𝐴 ) )
6	4 5	mpdan	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 +𝑒 - 𝐴 ) = ( 𝐴 + - 𝐴 ) )
7		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
8	7	negidd	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + - 𝐴 ) = 0 )
9	3 6 8	3eqtrd	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 +𝑒 -𝑒 𝐴 ) = 0 )
10		id	⊢ ( 𝐴 = +∞ → 𝐴 = +∞ )
11		xnegeq	⊢ ( 𝐴 = +∞ → -𝑒 𝐴 = -𝑒 +∞ )
12		xnegpnf	⊢ -𝑒 +∞ = -∞
13	11 12	eqtrdi	⊢ ( 𝐴 = +∞ → -𝑒 𝐴 = -∞ )
14	10 13	oveq12d	⊢ ( 𝐴 = +∞ → ( 𝐴 +𝑒 -𝑒 𝐴 ) = ( +∞ +𝑒 -∞ ) )
15		pnfaddmnf	⊢ ( +∞ +𝑒 -∞ ) = 0
16	14 15	eqtrdi	⊢ ( 𝐴 = +∞ → ( 𝐴 +𝑒 -𝑒 𝐴 ) = 0 )
17		id	⊢ ( 𝐴 = -∞ → 𝐴 = -∞ )
18		xnegeq	⊢ ( 𝐴 = -∞ → -𝑒 𝐴 = -𝑒 -∞ )
19		xnegmnf	⊢ -𝑒 -∞ = +∞
20	18 19	eqtrdi	⊢ ( 𝐴 = -∞ → -𝑒 𝐴 = +∞ )
21	17 20	oveq12d	⊢ ( 𝐴 = -∞ → ( 𝐴 +𝑒 -𝑒 𝐴 ) = ( -∞ +𝑒 +∞ ) )
22		mnfaddpnf	⊢ ( -∞ +𝑒 +∞ ) = 0
23	21 22	eqtrdi	⊢ ( 𝐴 = -∞ → ( 𝐴 +𝑒 -𝑒 𝐴 ) = 0 )
24	9 16 23	3jaoi	⊢ ( ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) → ( 𝐴 +𝑒 -𝑒 𝐴 ) = 0 )
25	1 24	sylbi	⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 +𝑒 -𝑒 𝐴 ) = 0 )