Metamath Proof Explorer

Theorem xnegcl

Description: Closure of extended real negative. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xnegcl 
|- ( A e. RR* -> -e A e. RR* )

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 renegcl 
 |-  ( A e. RR -> -u A e. RR )
4 2 3 eqeltrd 
 |-  ( A e. RR -> -e A e. RR )
5 4 rexrd 
 |-  ( A e. RR -> -e A e. RR* )
6 xnegeq 
 |-  ( A = +oo -> -e A = -e +oo )
7 xnegpnf 
 |-  -e +oo = -oo
8 mnfxr 
 |-  -oo e. RR*
9 7 8 eqeltri 
 |-  -e +oo e. RR*
10 6 9 eqeltrdi 
 |-  ( A = +oo -> -e A e. RR* )
11 xnegeq 
 |-  ( A = -oo -> -e A = -e -oo )
12 xnegmnf 
 |-  -e -oo = +oo
13 pnfxr 
 |-  +oo e. RR*
14 12 13 eqeltri 
 |-  -e -oo e. RR*
15 11 14 eqeltrdi 
 |-  ( A = -oo -> -e A e. RR* )
16 5 10 15 3jaoi 
 |-  ( ( A e. RR \/ A = +oo \/ A = -oo ) -> -e A e. RR* )
17 1 16 sylbi 
 |-  ( A e. RR* -> -e A e. RR* )