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

Theorem renegcld 11583
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 11465 . 2 (𝐴 ∈ ℝ → -𝐴 ∈ ℝ)
31, 2syl 17 1 (𝜑 → -𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  cr 11051  -cneg 11387
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-resscn 11109  ax-1cn 11110  ax-icn 11111  ax-addcl 11112  ax-addrcl 11113  ax-mulcl 11114  ax-mulrcl 11115  ax-mulcom 11116  ax-addass 11117  ax-mulass 11118  ax-distr 11119  ax-i2m1 11120  ax-1ne0 11121  ax-1rid 11122  ax-rnegex 11123  ax-rrecex 11124  ax-cnre 11125  ax-pre-lttri 11126  ax-pre-lttrn 11127  ax-pre-ltadd 11128
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-reu 3355  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-po 5546  df-so 5547  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-er 8649  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11192  df-mnf 11193  df-ltxr 11195  df-sub 11388  df-neg 11389
This theorem is referenced by:  ltord2  11685  leord2  11686  eqord2  11687  possumd  11781  recgt0  12002  riotaneg  12135  negiso  12136  nn0negleid  12466  difgtsumgt  12467  nnnegz  12503  prodge0rd  13023  modsub12d  13834  monoord2  13940  discr1  14143  discr  14144  recj  15010  reneg  15011  imcj  15018  imneg  15019  abslt  15200  absle  15201  o1lo1  15420  o1lo12  15421  icco1  15423  rlimrege0  15462  lo1sub  15514  iseraltlem2  15568  infcvgaux1i  15743  absefib  16081  efieq1re  16082  moddvds  16148  bitscmp  16319  bitsinv1lem  16322  mulgnegnn  18887  cnsubrg  20860  xrhmeo  24312  pjthlem1  24804  ivth2  24822  ovolshft  24878  shftmbl  24905  volsup2  24972  volivth  24974  mbfmulc2lem  25014  mbfposr  25019  mbfposb  25020  ismbf3d  25021  mbfmulc2  25030  mbfinf  25032  mbfi1fseqlem4  25086  mbfi1fseqlem5  25087  mbfi1fseqlem6  25088  mbfi1flimlem  25090  itg2monolem1  25118  iblposlem  25159  iblre  25161  itgreval  25164  itgneg  25171  i1fibl  25175  itgitg1  25176  itgle  25177  ibladd  25188  itgaddlem2  25191  iblabslem  25195  itgmulc2lem2  25200  itgmulc2  25201  bddiblnc  25209  dvferm2lem  25353  dvferm2  25354  rolle  25357  dvivth  25377  lhop2  25382  dvfsumge  25389  dvfsumlem2  25394  dvfsum2  25401  coseq0negpitopi  25863  tanabsge  25866  tanord  25897  tanregt0  25898  abslogimle  25932  logcj  25964  argimgt0  25970  logdiv2  25975  logcnlem3  26002  logccv  26021  abscxpbnd  26109  logreclem  26115  asinlem3a  26223  asinneg  26239  atanlogsublem  26268  atantan  26276  atans2  26284  birthdaylem3  26306  cxplim  26324  amgmlem  26342  emcllem7  26354  zetacvg  26367  eldmgm  26374  lgamgulmlem2  26382  lgsneg  26672  lgsdilem  26675  lgseisenlem1  26726  pntpbnd1  26937  pntibndlem2  26942  padicabvcxp  26983  ostth3  26989  axsegconlem9  27877  nvabs  29617  pjhthlem1  30336  xlt2addrd  31666  ccfldextdgrr  32359  xrge0iifcnv  32517  xrge0iifiso  32519  xrge0iifhom  32521  dya2ub  32873  sgnmul  33145  signsply0  33166  fdvneggt  33216  fdvnegge  33218  climlec3  34309  poimirlem29  36110  itg2gt0cn  36136  ibladdnc  36138  itgaddnclem2  36140  iblabsnclem  36144  itgmulc2nclem2  36148  itgmulc2nc  36149  ftc1anclem5  36158  dvasin  36165  areacirclem1  36169  areacirclem4  36172  areacirclem5  36173  areacirc  36174  oexpreposd  40810  3cubeslem4  41015  pellexlem6  41160  pell1234qrdich  41187  acongeq  41310  sqrtcval  41920  radcnvrat  42601  binomcxplemdvbinom  42640  binomcxplemnotnn0  42643  infnsuprnmpt  43485  neglt  43525  fperiodmul  43545  supsubc  43594  ltmulneg  43634  rexabslelem  43660  supminfrnmpt  43687  leneg2d  43690  leneg3d  43699  supminfxr  43706  climliminflimsupd  44049  liminfreuzlem  44050  liminfltlem  44052  stoweidlem1  44249  stoweidlem7  44255  stoweidlem13  44261  stoweidlem23  44271  stoweidlem34  44282  stoweidlem42  44290  stoweidlem47  44295  stirlinglem6  44327  stirlinglem10  44331  fourierdlem24  44379  fourierdlem39  44394  fourierdlem40  44395  fourierdlem43  44398  fourierdlem44  44399  fourierdlem46  44400  fourierdlem48  44402  fourierdlem49  44403  fourierdlem58  44412  fourierdlem62  44416  fourierdlem72  44426  fourierdlem78  44432  fourierdlem83  44437  fourierdlem85  44439  fourierdlem88  44442  fourierdlem92  44446  fourierdlem97  44451  fourierdlem103  44457  fourierdlem104  44458  fourierdlem109  44463  fourierdlem111  44465  fourierdlem112  44466  sqwvfoura  44476  etransclem23  44505  etransclem46  44528  hoicvr  44796  hoicvrrex  44804  smfinflem  45065  smfliminflem  45078  finfdm  45094  smfinfdmmbllem  45096  sigaradd  45114  sqrtnegnre  45546  proththd  45813  requad01  45820  requad1  45821  requad2  45822  dignn0flhalflem1  46708  eenglngeehlnmlem1  46830  eenglngeehlnmlem2  46831  line2ylem  46844  itscnhlc0yqe  46852  itsclquadb  46869  itscnhlinecirc02p  46878  amgmwlem  47256
  Copyright terms: Public domain W3C validator