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 
|- ( A e. RR* -> -e -e A = A )

Proof

Step Hyp Ref Expression
1 elxr 
 |-  ( A e. RR* <-> ( A e. RR \/ A = +oo \/ A = -oo ) )
2 rexneg 
 |-  ( A e. RR -> -e A = -u A )
3 xnegeq 
 |-  ( -e A = -u A -> -e -e A = -e -u A )
4 2 3 syl 
 |-  ( A e. RR -> -e -e A = -e -u A )
5 renegcl 
 |-  ( A e. RR -> -u A e. RR )
6 rexneg 
 |-  ( -u A e. RR -> -e -u A = -u -u A )
7 5 6 syl 
 |-  ( A e. RR -> -e -u A = -u -u A )
8 recn 
 |-  ( A e. RR -> A e. CC )
9 8 negnegd 
 |-  ( A e. RR -> -u -u A = A )
10 4 7 9 3eqtrd 
 |-  ( A e. RR -> -e -e A = A )
11 xnegmnf 
 |-  -e -oo = +oo
12 xnegeq 
 |-  ( A = +oo -> -e A = -e +oo )
13 xnegpnf 
 |-  -e +oo = -oo
14 12 13 eqtrdi 
 |-  ( A = +oo -> -e A = -oo )
15 xnegeq 
 |-  ( -e A = -oo -> -e -e A = -e -oo )
16 14 15 syl 
 |-  ( A = +oo -> -e -e A = -e -oo )
17 id 
 |-  ( A = +oo -> A = +oo )
18 11 16 17 3eqtr4a 
 |-  ( A = +oo -> -e -e A = A )
19 xnegeq 
 |-  ( A = -oo -> -e A = -e -oo )
20 19 11 eqtrdi 
 |-  ( A = -oo -> -e A = +oo )
21 xnegeq 
 |-  ( -e A = +oo -> -e -e A = -e +oo )
22 20 21 syl 
 |-  ( A = -oo -> -e -e A = -e +oo )
23 id 
 |-  ( A = -oo -> A = -oo )
24 13 22 23 3eqtr4a 
 |-  ( A = -oo -> -e -e A = A )
25 10 18 24 3jaoi 
 |-  ( ( A e. RR \/ A = +oo \/ A = -oo ) -> -e -e A = A )
26 1 25 sylbi 
 |-  ( A e. RR* -> -e -e A = A )