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

Theorem renegcld 9765
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 9662 . 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 1757   RRcr 9271   -ucneg 9586
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416  ax-sep 4403  ax-nul 4411  ax-pow 4460  ax-pr 4521  ax-un 6363  ax-resscn 9329  ax-1cn 9330  ax-icn 9331  ax-addcl 9332  ax-addrcl 9333  ax-mulcl 9334  ax-mulrcl 9335  ax-mulcom 9336  ax-addass 9337  ax-mulass 9338  ax-distr 9339  ax-i2m1 9340  ax-1ne0 9341  ax-1rid 9342  ax-rnegex 9343  ax-rrecex 9344  ax-cnre 9345  ax-pre-lttri 9346  ax-pre-lttrn 9347  ax-pre-ltadd 9348
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2966  df-sbc 3178  df-csb 3279  df-dif 3321  df-un 3323  df-in 3325  df-ss 3332  df-nul 3628  df-if 3782  df-pw 3852  df-sn 3868  df-pr 3870  df-op 3874  df-uni 4082  df-br 4283  df-opab 4341  df-mpt 4342  df-id 4625  df-po 4630  df-so 4631  df-xp 4835  df-rel 4836  df-cnv 4837  df-co 4838  df-dm 4839  df-rn 4840  df-res 4841  df-ima 4842  df-iota 5371  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-riota 6041  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-er 7091  df-en 7301  df-dom 7302  df-sdom 7303  df-pnf 9410  df-mnf 9411  df-ltxr 9413  df-sub 9587  df-neg 9588
This theorem is referenced by:  ltord2  9859  leord2  9860  eqord2  9861  recgt0  10163  prodge0  10166  riotaneg  10295  negiso  10296  infmrcl  10299  nnnegz  10639  modsub12d  11742  monoord2  11823  discr1  11986  discr  11987  recj  12599  reneg  12600  imcj  12607  imneg  12608  abslt  12788  absle  12789  o1lo1  13001  o1lo12  13002  icco1  13004  rlimrege0  13043  lo1sub  13094  iseraltlem2  13146  infcvgaux1i  13304  absefib  13467  efieq1re  13468  moddvds  13527  bitscmp  13619  bitsinv1lem  13622  mulgnegnn  15619  cnsubrg  17719  xrhmeo  20362  pjthlem1  20768  ivth2  20783  ovolshft  20838  shftmbl  20864  volsup2  20929  volivth  20931  mbfmulc2lem  20969  mbfposr  20974  mbfposb  20975  ismbf3d  20976  mbfmulc2  20985  mbfinf  20987  mbfi1fseqlem4  21040  mbfi1fseqlem5  21041  mbfi1fseqlem6  21042  mbfi1flimlem  21044  itg2monolem1  21072  iblposlem  21113  iblre  21115  itgreval  21118  itgneg  21125  i1fibl  21129  itgitg1  21130  itgle  21131  ibladd  21142  itgaddlem2  21145  iblabslem  21149  itgmulc2lem2  21154  itgmulc2  21155  dvferm2lem  21302  dvferm2  21303  rolle  21306  dvivth  21326  lhop2  21331  dvfsumge  21338  dvfsumlem2  21343  dvfsum2  21350  coseq0negpitopi  21852  tanabsge  21855  tanord  21881  tanregt0  21882  abslogimle  21912  logcj  21942  argimgt0  21948  logdiv2  21953  logcnlem3  21976  dvloglem  21980  logccv  21995  abscxpbnd  22078  logreclem  22101  asinlem3a  22152  asinneg  22168  atanlogsublem  22197  atantan  22205  atans2  22213  birthdaylem3  22234  cxplim  22252  amgmlem  22270  emcllem7  22282  lgsneg  22545  lgsdilem  22548  lgseisenlem1  22575  pntpbnd1  22722  pntibndlem2  22727  padicabvcxp  22768  ostth3  22774  axsegconlem9  22996  nvabs  23886  pjhthlem1  24619  xlt2addrd  25878  xrge0iifcnv  26219  xrge0iifiso  26221  xrge0iifhom  26223  dya2ub  26541  sgnmul  26775  signsply0  26802  zetacvg  26851  eldmgm  26858  lgamgulmlem2  26866  possumd  27245  climlec3  27250  itg2gt0cn  28293  ibladdnc  28295  itgaddnclem2  28297  iblabsnclem  28301  itgmulc2nclem2  28305  itgmulc2nc  28306  bddiblnc  28308  ftc1anclem5  28317  dvasin  28326  areacirclem1  28330  areacirclem4  28333  areacirclem5  28334  areacirc  28335  pellexlem6  29022  pell1234qrdich  29049  acongeq  29173  stoweidlem1  29644  stoweidlem7  29650  stoweidlem13  29656  stoweidlem23  29666  stoweidlem34  29677  stoweidlem42  29685  stoweidlem47  29690  stirlinglem6  29722  stirlinglem10  29726  sigaradd  29750
  Copyright terms: Public domain W3C validator