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

Theorem renegcld 10442
Description: Closure law for negative of reals. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
renegcld.1 (𝜑𝐴 ∈ ℝ)
Assertion
Ref Expression
renegcld (𝜑 → -𝐴 ∈ ℝ)

Proof of Theorem renegcld
StepHypRef Expression
1 renegcld.1 . 2 (𝜑𝐴 ∈ ℝ)
2 renegcl 10329 . 2 (𝐴 ∈ ℝ → -𝐴 ∈ ℝ)
31, 2syl 17 1 (𝜑 → -𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1988  cr 9920  -cneg 10252
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-mpt 4721  df-id 5014  df-po 5025  df-so 5026  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-er 7727  df-en 7941  df-dom 7942  df-sdom 7943  df-pnf 10061  df-mnf 10062  df-ltxr 10064  df-sub 10253  df-neg 10254
This theorem is referenced by:  ltord2  10542  leord2  10543  eqord2  10544  possumd  10637  recgt0  10852  prodge0  10855  riotaneg  10987  negiso  10988  nn0negleid  11330  difgtsumgt  11331  nnnegz  11365  modsub12d  12710  monoord2  12815  discr1  12983  discr  12984  recj  13845  reneg  13846  imcj  13853  imneg  13854  abslt  14035  absle  14036  o1lo1  14249  o1lo12  14250  icco1  14252  rlimrege0  14291  lo1sub  14342  iseraltlem2  14394  infcvgaux1i  14570  absefib  14909  efieq1re  14910  moddvds  14972  bitscmp  15141  bitsinv1lem  15144  mulgnegnn  17532  cnsubrg  19787  xrhmeo  22726  pjthlem1  23189  ivth2  23205  ovolshft  23260  shftmbl  23287  volsup2  23354  volivth  23356  mbfmulc2lem  23395  mbfposr  23400  mbfposb  23401  ismbf3d  23402  mbfmulc2  23411  mbfinf  23413  mbfi1fseqlem4  23466  mbfi1fseqlem5  23467  mbfi1fseqlem6  23468  mbfi1flimlem  23470  itg2monolem1  23498  iblposlem  23539  iblre  23541  itgreval  23544  itgneg  23551  i1fibl  23555  itgitg1  23556  itgle  23557  ibladd  23568  itgaddlem2  23571  iblabslem  23575  itgmulc2lem2  23580  itgmulc2  23581  dvferm2lem  23730  dvferm2  23731  rolle  23734  dvivth  23754  lhop2  23759  dvfsumge  23766  dvfsumlem2  23771  dvfsum2  23778  coseq0negpitopi  24236  tanabsge  24239  tanord  24265  tanregt0  24266  abslogimle  24301  logcj  24333  argimgt0  24339  logdiv2  24344  logcnlem3  24371  dvloglem  24375  logccv  24390  abscxpbnd  24475  logreclem  24481  asinlem3a  24578  asinneg  24594  atanlogsublem  24623  atantan  24631  atans2  24639  birthdaylem3  24661  cxplim  24679  amgmlem  24697  emcllem7  24709  zetacvg  24722  eldmgm  24729  lgamgulmlem2  24737  lgsneg  25027  lgsdilem  25030  lgseisenlem1  25081  pntpbnd1  25256  pntibndlem2  25261  padicabvcxp  25302  ostth3  25308  axsegconlem9  25786  nvabs  27497  pjhthlem1  28220  xlt2addrd  29497  xrge0iifcnv  29953  xrge0iifiso  29955  xrge0iifhom  29957  dya2ub  30306  sgnmul  30578  signsply0  30602  fdvneggt  30652  fdvnegge  30654  climlec3  31594  poimirlem29  33409  itg2gt0cn  33436  ibladdnc  33438  itgaddnclem2  33440  iblabsnclem  33444  itgmulc2nclem2  33448  itgmulc2nc  33449  bddiblnc  33451  ftc1anclem5  33460  dvasin  33467  areacirclem1  33471  areacirclem4  33474  areacirclem5  33475  areacirc  33476  pellexlem6  37217  pell1234qrdich  37244  acongeq  37369  radcnvrat  38333  binomcxplemdvbinom  38372  binomcxplemnotnn0  38375  infnsuprnmpt  39281  neglt  39309  fperiodmul  39331  supsubc  39382  ltmulneg  39428  rexabslelem  39458  supminfrnmpt  39485  leneg2d  39489  leneg3d  39500  supminfxr  39507  climliminflimsupd  39827  liminfreuzlem  39828  liminfltlem  39830  stoweidlem1  39981  stoweidlem7  39987  stoweidlem13  39993  stoweidlem23  40003  stoweidlem34  40014  stoweidlem42  40022  stoweidlem47  40027  stirlinglem6  40059  stirlinglem10  40063  fourierdlem24  40111  fourierdlem39  40126  fourierdlem40  40127  fourierdlem43  40130  fourierdlem44  40131  fourierdlem46  40132  fourierdlem48  40134  fourierdlem49  40135  fourierdlem58  40144  fourierdlem62  40148  fourierdlem72  40158  fourierdlem78  40164  fourierdlem83  40169  fourierdlem85  40171  fourierdlem88  40174  fourierdlem92  40178  fourierdlem97  40183  fourierdlem103  40189  fourierdlem104  40190  fourierdlem109  40195  fourierdlem111  40197  fourierdlem112  40198  sqwvfoura  40208  etransclem23  40237  etransclem46  40260  hoicvr  40525  hoicvrrex  40533  smfinflem  40786  smfliminflem  40799  sigaradd  40818  proththd  41296  dignn0flhalflem1  42174  amgmwlem  42313
  Copyright terms: Public domain W3C validator