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

Theorem renegcld 10303
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 10190 . 2 (𝐴 ∈ ℝ → -𝐴 ∈ ℝ)
31, 2syl 17 1 (𝜑 → -𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1975  cr 9786  -cneg 10113
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2227  ax-ext 2584  ax-sep 4698  ax-nul 4707  ax-pow 4759  ax-pr 4823  ax-un 6819  ax-resscn 9844  ax-1cn 9845  ax-icn 9846  ax-addcl 9847  ax-addrcl 9848  ax-mulcl 9849  ax-mulrcl 9850  ax-mulcom 9851  ax-addass 9852  ax-mulass 9853  ax-distr 9854  ax-i2m1 9855  ax-1ne0 9856  ax-1rid 9857  ax-rnegex 9858  ax-rrecex 9859  ax-cnre 9860  ax-pre-lttri 9861  ax-pre-lttrn 9862  ax-pre-ltadd 9863
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2456  df-mo 2457  df-clab 2591  df-cleq 2597  df-clel 2600  df-nfc 2734  df-ne 2776  df-nel 2777  df-ral 2895  df-rex 2896  df-reu 2897  df-rab 2899  df-v 3169  df-sbc 3397  df-csb 3494  df-dif 3537  df-un 3539  df-in 3541  df-ss 3548  df-nul 3869  df-if 4031  df-pw 4104  df-sn 4120  df-pr 4122  df-op 4126  df-uni 4362  df-br 4573  df-opab 4633  df-mpt 4634  df-id 4938  df-po 4944  df-so 4945  df-xp 5029  df-rel 5030  df-cnv 5031  df-co 5032  df-dm 5033  df-rn 5034  df-res 5035  df-ima 5036  df-iota 5749  df-fun 5787  df-fn 5788  df-f 5789  df-f1 5790  df-fo 5791  df-f1o 5792  df-fv 5793  df-riota 6484  df-ov 6525  df-oprab 6526  df-mpt2 6527  df-er 7601  df-en 7814  df-dom 7815  df-sdom 7816  df-pnf 9927  df-mnf 9928  df-ltxr 9930  df-sub 10114  df-neg 10115
This theorem is referenced by:  ltord2  10401  leord2  10402  eqord2  10403  possumd  10496  recgt0  10711  prodge0  10714  riotaneg  10844  negiso  10845  nn0negleid  11187  difgtsumgt  11188  nnnegz  11208  modsub12d  12539  monoord2  12644  discr1  12812  discr  12813  recj  13653  reneg  13654  imcj  13661  imneg  13662  abslt  13843  absle  13844  o1lo1  14057  o1lo12  14058  icco1  14060  rlimrege0  14099  lo1sub  14150  iseraltlem2  14202  infcvgaux1i  14369  absefib  14708  efieq1re  14709  moddvds  14770  bitscmp  14939  bitsinv1lem  14942  mulgnegnn  17315  cnsubrg  19566  xrhmeo  22479  pjthlem1  22928  ivth2  22943  ovolshft  22998  shftmbl  23025  volsup2  23091  volivth  23093  mbfmulc2lem  23132  mbfposr  23137  mbfposb  23138  ismbf3d  23139  mbfmulc2  23148  mbfinf  23150  mbfi1fseqlem4  23203  mbfi1fseqlem5  23204  mbfi1fseqlem6  23205  mbfi1flimlem  23207  itg2monolem1  23235  iblposlem  23276  iblre  23278  itgreval  23281  itgneg  23288  i1fibl  23292  itgitg1  23293  itgle  23294  ibladd  23305  itgaddlem2  23308  iblabslem  23312  itgmulc2lem2  23317  itgmulc2  23318  dvferm2lem  23465  dvferm2  23466  rolle  23469  dvivth  23489  lhop2  23494  dvfsumge  23501  dvfsumlem2  23506  dvfsum2  23513  coseq0negpitopi  23971  tanabsge  23974  tanord  24000  tanregt0  24001  abslogimle  24036  logcj  24068  argimgt0  24074  logdiv2  24079  logcnlem3  24102  dvloglem  24106  logccv  24121  abscxpbnd  24206  logreclem  24212  asinlem3a  24309  asinneg  24325  atanlogsublem  24354  atantan  24362  atans2  24370  birthdaylem3  24392  cxplim  24410  amgmlem  24428  emcllem7  24440  zetacvg  24453  eldmgm  24460  lgamgulmlem2  24468  lgsneg  24758  lgsdilem  24761  lgseisenlem1  24812  pntpbnd1  24987  pntibndlem2  24992  padicabvcxp  25033  ostth3  25039  axsegconlem9  25518  nvabs  26701  pjhthlem1  27435  xlt2addrd  28714  xrge0iifcnv  29108  xrge0iifiso  29110  xrge0iifhom  29112  dya2ub  29460  sgnmul  29732  signsply0  29755  climlec3  30673  poimirlem29  32406  itg2gt0cn  32433  ibladdnc  32435  itgaddnclem2  32437  iblabsnclem  32441  itgmulc2nclem2  32445  itgmulc2nc  32446  bddiblnc  32448  ftc1anclem5  32457  dvasin  32464  areacirclem1  32468  areacirclem4  32471  areacirclem5  32472  areacirc  32473  pellexlem6  36214  pell1234qrdich  36241  acongeq  36366  radcnvrat  37333  binomcxplemdvbinom  37372  binomcxplemnotnn0  37375  neglt  38235  fperiodmul  38257  supsubc  38309  ltmulneg  38355  stoweidlem1  38693  stoweidlem7  38699  stoweidlem13  38705  stoweidlem23  38715  stoweidlem34  38726  stoweidlem42  38734  stoweidlem47  38739  stirlinglem6  38771  stirlinglem10  38775  fourierdlem24  38823  fourierdlem39  38838  fourierdlem40  38839  fourierdlem43  38842  fourierdlem44  38843  fourierdlem46  38844  fourierdlem48  38846  fourierdlem49  38847  fourierdlem58  38856  fourierdlem62  38860  fourierdlem72  38870  fourierdlem78  38876  fourierdlem83  38881  fourierdlem85  38883  fourierdlem88  38886  fourierdlem92  38890  fourierdlem97  38895  fourierdlem103  38901  fourierdlem104  38902  fourierdlem109  38907  fourierdlem111  38909  fourierdlem112  38910  sqwvfoura  38920  etransclem23  38949  etransclem46  38972  hoicvr  39237  hoicvrrex  39245  sigaradd  39503  proththd  39869  dignn0flhalflem1  42204  amgmwlem  42315
  Copyright terms: Public domain W3C validator