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

Metamath Proof Explorer

Theorem xnegneg

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

Ref Expression
Assertion xnegneg ( 𝐴 ∈ ℝ* → -𝑒 -𝑒 𝐴 = 𝐴 )

Proof

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