MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  renegcld Structured version   Unicode version

Theorem renegcld 9887
Description: Closure law for negative of reals. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
renegcld.1  |-  ( ph  ->  A  e.  RR )
Assertion
Ref Expression
renegcld  |-  ( ph  -> 
-u A  e.  RR )

Proof of Theorem renegcld
StepHypRef Expression
1 renegcld.1 . 2  |-  ( ph  ->  A  e.  RR )
2 renegcl 9784 . 2  |-  ( A  e.  RR  ->  -u A  e.  RR )
31, 2syl 16 1  |-  ( ph  -> 
-u A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1758   RRcr 9393   -ucneg 9708
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4522  ax-nul 4530  ax-pow 4579  ax-pr 4640  ax-un 6483  ax-resscn 9451  ax-1cn 9452  ax-icn 9453  ax-addcl 9454  ax-addrcl 9455  ax-mulcl 9456  ax-mulrcl 9457  ax-mulcom 9458  ax-addass 9459  ax-mulass 9460  ax-distr 9461  ax-i2m1 9462  ax-1ne0 9463  ax-1rid 9464  ax-rnegex 9465  ax-rrecex 9466  ax-cnre 9467  ax-pre-lttri 9468  ax-pre-lttrn 9469  ax-pre-ltadd 9470
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-nel 2651  df-ral 2804  df-rex 2805  df-reu 2806  df-rab 2808  df-v 3080  df-sbc 3295  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3747  df-if 3901  df-pw 3971  df-sn 3987  df-pr 3989  df-op 3993  df-uni 4201  df-br 4402  df-opab 4460  df-mpt 4461  df-id 4745  df-po 4750  df-so 4751  df-xp 4955  df-rel 4956  df-cnv 4957  df-co 4958  df-dm 4959  df-rn 4960  df-res 4961  df-ima 4962  df-iota 5490  df-fun 5529  df-fn 5530  df-f 5531  df-f1 5532  df-fo 5533  df-f1o 5534  df-fv 5535  df-riota 6162  df-ov 6204  df-oprab 6205  df-mpt2 6206  df-er 7212  df-en 7422  df-dom 7423  df-sdom 7424  df-pnf 9532  df-mnf 9533  df-ltxr 9535  df-sub 9709  df-neg 9710
This theorem is referenced by:  ltord2  9981  leord2  9982  eqord2  9983  recgt0  10285  prodge0  10288  riotaneg  10417  negiso  10418  infmrcl  10421  nnnegz  10761  modsub12d  11874  monoord2  11955  discr1  12118  discr  12119  recj  12732  reneg  12733  imcj  12740  imneg  12741  abslt  12921  absle  12922  o1lo1  13134  o1lo12  13135  icco1  13137  rlimrege0  13176  lo1sub  13227  iseraltlem2  13279  infcvgaux1i  13438  absefib  13601  efieq1re  13602  moddvds  13661  bitscmp  13753  bitsinv1lem  13756  mulgnegnn  15757  cnsubrg  17999  xrhmeo  20651  pjthlem1  21057  ivth2  21072  ovolshft  21127  shftmbl  21154  volsup2  21219  volivth  21221  mbfmulc2lem  21259  mbfposr  21264  mbfposb  21265  ismbf3d  21266  mbfmulc2  21275  mbfinf  21277  mbfi1fseqlem4  21330  mbfi1fseqlem5  21331  mbfi1fseqlem6  21332  mbfi1flimlem  21334  itg2monolem1  21362  iblposlem  21403  iblre  21405  itgreval  21408  itgneg  21415  i1fibl  21419  itgitg1  21420  itgle  21421  ibladd  21432  itgaddlem2  21435  iblabslem  21439  itgmulc2lem2  21444  itgmulc2  21445  dvferm2lem  21592  dvferm2  21593  rolle  21596  dvivth  21616  lhop2  21621  dvfsumge  21628  dvfsumlem2  21633  dvfsum2  21640  coseq0negpitopi  22099  tanabsge  22102  tanord  22128  tanregt0  22129  abslogimle  22159  logcj  22189  argimgt0  22195  logdiv2  22200  logcnlem3  22223  dvloglem  22227  logccv  22242  abscxpbnd  22325  logreclem  22348  asinlem3a  22399  asinneg  22415  atanlogsublem  22444  atantan  22452  atans2  22460  birthdaylem3  22481  cxplim  22499  amgmlem  22517  emcllem7  22529  lgsneg  22792  lgsdilem  22795  lgseisenlem1  22822  pntpbnd1  22969  pntibndlem2  22974  padicabvcxp  23015  ostth3  23021  axsegconlem9  23324  nvabs  24214  pjhthlem1  24947  xlt2addrd  26203  xrge0iifcnv  26509  xrge0iifiso  26511  xrge0iifhom  26513  dya2ub  26830  sgnmul  27070  signsply0  27097  zetacvg  27146  eldmgm  27153  lgamgulmlem2  27161  possumd  27541  climlec3  27546  itg2gt0cn  28596  ibladdnc  28598  itgaddnclem2  28600  iblabsnclem  28604  itgmulc2nclem2  28608  itgmulc2nc  28609  bddiblnc  28611  ftc1anclem5  28620  dvasin  28629  areacirclem1  28633  areacirclem4  28636  areacirclem5  28637  areacirc  28638  pellexlem6  29324  pell1234qrdich  29351  acongeq  29475  stoweidlem1  29945  stoweidlem7  29951  stoweidlem13  29957  stoweidlem23  29967  stoweidlem34  29978  stoweidlem42  29986  stoweidlem47  29991  stirlinglem6  30023  stirlinglem10  30027  sigaradd  30051
  Copyright terms: Public domain W3C validator