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

Theorem renegcld 11066
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 10948 . 2 (𝐴 ∈ ℝ → -𝐴 ∈ ℝ)
31, 2syl 17 1 (𝜑 → -𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2110  cr 10535  -cneg 10870
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pow 5265  ax-pr 5329  ax-un 7460  ax-resscn 10593  ax-1cn 10594  ax-icn 10595  ax-addcl 10596  ax-addrcl 10597  ax-mulcl 10598  ax-mulrcl 10599  ax-mulcom 10600  ax-addass 10601  ax-mulass 10602  ax-distr 10603  ax-i2m1 10604  ax-1ne0 10605  ax-1rid 10606  ax-rnegex 10607  ax-rrecex 10608  ax-cnre 10609  ax-pre-lttri 10610  ax-pre-lttrn 10611  ax-pre-ltadd 10612
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4838  df-br 5066  df-opab 5128  df-mpt 5146  df-id 5459  df-po 5473  df-so 5474  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-riota 7113  df-ov 7158  df-oprab 7159  df-mpo 7160  df-er 8288  df-en 8509  df-dom 8510  df-sdom 8511  df-pnf 10676  df-mnf 10677  df-ltxr 10679  df-sub 10871  df-neg 10872
This theorem is referenced by:  ltord2  11168  leord2  11169  eqord2  11170  possumd  11264  recgt0  11485  riotaneg  11619  negiso  11620  nn0negleid  11948  difgtsumgt  11949  nnnegz  11983  prodge0rd  12495  modsub12d  13295  monoord2  13400  discr1  13599  discr  13600  recj  14482  reneg  14483  imcj  14490  imneg  14491  abslt  14673  absle  14674  o1lo1  14893  o1lo12  14894  icco1  14896  rlimrege0  14935  lo1sub  14986  iseraltlem2  15038  infcvgaux1i  15211  absefib  15550  efieq1re  15551  moddvds  15617  bitscmp  15786  bitsinv1lem  15789  mulgnegnn  18237  cnsubrg  20604  xrhmeo  23549  pjthlem1  24039  ivth2  24055  ovolshft  24111  shftmbl  24138  volsup2  24205  volivth  24207  mbfmulc2lem  24247  mbfposr  24252  mbfposb  24253  ismbf3d  24254  mbfmulc2  24263  mbfinf  24265  mbfi1fseqlem4  24318  mbfi1fseqlem5  24319  mbfi1fseqlem6  24320  mbfi1flimlem  24322  itg2monolem1  24350  iblposlem  24391  iblre  24393  itgreval  24396  itgneg  24403  i1fibl  24407  itgitg1  24408  itgle  24409  ibladd  24420  itgaddlem2  24423  iblabslem  24427  itgmulc2lem2  24432  itgmulc2  24433  dvferm2lem  24582  dvferm2  24583  rolle  24586  dvivth  24606  lhop2  24611  dvfsumge  24618  dvfsumlem2  24623  dvfsum2  24630  coseq0negpitopi  25088  tanabsge  25091  tanord  25121  tanregt0  25122  abslogimle  25156  logcj  25188  argimgt0  25194  logdiv2  25199  logcnlem3  25226  logccv  25245  abscxpbnd  25333  logreclem  25339  asinlem3a  25447  asinneg  25463  atanlogsublem  25492  atantan  25500  atans2  25508  birthdaylem3  25530  cxplim  25548  amgmlem  25566  emcllem7  25578  zetacvg  25591  eldmgm  25598  lgamgulmlem2  25606  lgsneg  25896  lgsdilem  25899  lgseisenlem1  25950  pntpbnd1  26161  pntibndlem2  26166  padicabvcxp  26207  ostth3  26213  axsegconlem9  26710  nvabs  28448  pjhthlem1  29167  xlt2addrd  30481  ccfldextdgrr  31057  xrge0iifcnv  31176  xrge0iifiso  31178  xrge0iifhom  31180  dya2ub  31528  sgnmul  31800  signsply0  31821  fdvneggt  31871  fdvnegge  31873  climlec3  32965  poimirlem29  34920  itg2gt0cn  34946  ibladdnc  34948  itgaddnclem2  34950  iblabsnclem  34954  itgmulc2nclem2  34958  itgmulc2nc  34959  bddiblnc  34961  ftc1anclem5  34970  dvasin  34977  areacirclem1  34981  areacirclem4  34984  areacirclem5  34985  areacirc  34986  oexpreposd  39177  3cubeslem4  39284  pellexlem6  39429  pell1234qrdich  39456  acongeq  39578  radcnvrat  40644  binomcxplemdvbinom  40683  binomcxplemnotnn0  40686  infnsuprnmpt  41520  neglt  41548  fperiodmul  41569  supsubc  41619  ltmulneg  41662  rexabslelem  41690  supminfrnmpt  41717  leneg2d  41721  leneg3d  41731  supminfxr  41738  climliminflimsupd  42080  liminfreuzlem  42081  liminfltlem  42083  stoweidlem1  42285  stoweidlem7  42291  stoweidlem13  42297  stoweidlem23  42307  stoweidlem34  42318  stoweidlem42  42326  stoweidlem47  42331  stirlinglem6  42363  stirlinglem10  42367  fourierdlem24  42415  fourierdlem39  42430  fourierdlem40  42431  fourierdlem43  42434  fourierdlem44  42435  fourierdlem46  42436  fourierdlem48  42438  fourierdlem49  42439  fourierdlem58  42448  fourierdlem62  42452  fourierdlem72  42462  fourierdlem78  42468  fourierdlem83  42473  fourierdlem85  42475  fourierdlem88  42478  fourierdlem92  42482  fourierdlem97  42487  fourierdlem103  42493  fourierdlem104  42494  fourierdlem109  42499  fourierdlem111  42501  fourierdlem112  42502  sqwvfoura  42512  etransclem23  42541  etransclem46  42564  hoicvr  42829  hoicvrrex  42837  smfinflem  43090  smfliminflem  43103  sigaradd  43122  sqrtnegnre  43506  proththd  43778  requad01  43785  requad1  43786  requad2  43787  dignn0flhalflem1  44674  eenglngeehlnmlem1  44723  eenglngeehlnmlem2  44724  line2ylem  44737  itscnhlc0yqe  44745  itsclquadb  44762  itscnhlinecirc02p  44771  amgmwlem  44902
  Copyright terms: Public domain W3C validator