This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )