Metamath Proof Explorer


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 )