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 )