ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  xnegcl Unicode version

Theorem xnegcl 9762
Description: Closure of extended real negative. (Contributed by Mario Carneiro, 20-Aug-2015.)
Assertion
Ref Expression
xnegcl  |-  ( A  e.  RR*  ->  -e
A  e.  RR* )

Proof of Theorem xnegcl
StepHypRef Expression
1 elxr 9706 . 2  |-  ( A  e.  RR*  <->  ( A  e.  RR  \/  A  = +oo  \/  A  = -oo ) )
2 rexneg 9760 . . . . 5  |-  ( A  e.  RR  ->  -e
A  =  -u A
)
3 renegcl 8153 . . . . 5  |-  ( A  e.  RR  ->  -u A  e.  RR )
42, 3eqeltrd 2241 . . . 4  |-  ( A  e.  RR  ->  -e
A  e.  RR )
54rexrd 7942 . . 3  |-  ( A  e.  RR  ->  -e
A  e.  RR* )
6 xnegeq 9757 . . . 4  |-  ( A  = +oo  ->  -e
A  =  -e +oo )
7 xnegpnf 9758 . . . . 5  |-  -e +oo  = -oo
8 mnfxr 7949 . . . . 5  |- -oo  e.  RR*
97, 8eqeltri 2237 . . . 4  |-  -e +oo  e.  RR*
106, 9eqeltrdi 2255 . . 3  |-  ( A  = +oo  ->  -e
A  e.  RR* )
11 xnegeq 9757 . . . 4  |-  ( A  = -oo  ->  -e
A  =  -e -oo )
12 xnegmnf 9759 . . . . 5  |-  -e -oo  = +oo
13 pnfxr 7945 . . . . 5  |- +oo  e.  RR*
1412, 13eqeltri 2237 . . . 4  |-  -e -oo  e.  RR*
1511, 14eqeltrdi 2255 . . 3  |-  ( A  = -oo  ->  -e
A  e.  RR* )
165, 10, 153jaoi 1292 . 2  |-  ( ( A  e.  RR  \/  A  = +oo  \/  A  = -oo )  ->  -e
A  e.  RR* )
171, 16sylbi 120 1  |-  ( A  e.  RR*  ->  -e
A  e.  RR* )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ w3o 966    = wceq 1342    e. wcel 2135   RRcr 7746   +oocpnf 7924   -oocmnf 7925   RR*cxr 7926   -ucneg 8064    -ecxne 9699
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-13 2137  ax-14 2138  ax-ext 2146  ax-sep 4097  ax-pow 4150  ax-pr 4184  ax-un 4408  ax-setind 4511  ax-cnex 7838  ax-resscn 7839  ax-1cn 7840  ax-icn 7842  ax-addcl 7843  ax-addrcl 7844  ax-mulcl 7845  ax-addcom 7847  ax-addass 7849  ax-distr 7851  ax-i2m1 7852  ax-0id 7855  ax-rnegex 7856  ax-cnre 7858
This theorem depends on definitions:  df-bi 116  df-3or 968  df-3an 969  df-tru 1345  df-fal 1348  df-nf 1448  df-sb 1750  df-eu 2016  df-mo 2017  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ne 2335  df-nel 2430  df-ral 2447  df-rex 2448  df-reu 2449  df-rab 2451  df-v 2726  df-sbc 2950  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-if 3519  df-pw 3558  df-sn 3579  df-pr 3580  df-op 3582  df-uni 3787  df-br 3980  df-opab 4041  df-id 4268  df-xp 4607  df-rel 4608  df-cnv 4609  df-co 4610  df-dm 4611  df-iota 5150  df-fun 5187  df-fv 5193  df-riota 5795  df-ov 5842  df-oprab 5843  df-mpo 5844  df-pnf 7929  df-mnf 7930  df-xr 7931  df-sub 8065  df-neg 8066  df-xneg 9702
This theorem is referenced by:  xltneg  9766  xleneg  9767  xnegcld  9785  xnegdi  9798  xaddass2  9800  xleadd1  9805  xsubge0  9811  xrnegiso  11197  xrminmax  11200  xrmincl  11201  xrmin1inf  11202  xrmin2inf  11203  xrlemininf  11206  xrminltinf  11207
  Copyright terms: Public domain W3C validator