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

Theorem renegcld 10647
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 10534 . 2 (𝐴 ∈ ℝ → -𝐴 ∈ ℝ)
31, 2syl 17 1 (𝜑 → -𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2137  cr 10125  -cneg 10457
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-8 2139  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-sep 4931  ax-nul 4939  ax-pow 4990  ax-pr 5053  ax-un 7112  ax-resscn 10183  ax-1cn 10184  ax-icn 10185  ax-addcl 10186  ax-addrcl 10187  ax-mulcl 10188  ax-mulrcl 10189  ax-mulcom 10190  ax-addass 10191  ax-mulass 10192  ax-distr 10193  ax-i2m1 10194  ax-1ne0 10195  ax-1rid 10196  ax-rnegex 10197  ax-rrecex 10198  ax-cnre 10199  ax-pre-lttri 10200  ax-pre-lttrn 10201  ax-pre-ltadd 10202
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-mo 2610  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ne 2931  df-nel 3034  df-ral 3053  df-rex 3054  df-reu 3055  df-rab 3057  df-v 3340  df-sbc 3575  df-csb 3673  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-nul 4057  df-if 4229  df-pw 4302  df-sn 4320  df-pr 4322  df-op 4326  df-uni 4587  df-br 4803  df-opab 4863  df-mpt 4880  df-id 5172  df-po 5185  df-so 5186  df-xp 5270  df-rel 5271  df-cnv 5272  df-co 5273  df-dm 5274  df-rn 5275  df-res 5276  df-ima 5277  df-iota 6010  df-fun 6049  df-fn 6050  df-f 6051  df-f1 6052  df-fo 6053  df-f1o 6054  df-fv 6055  df-riota 6772  df-ov 6814  df-oprab 6815  df-mpt2 6816  df-er 7909  df-en 8120  df-dom 8121  df-sdom 8122  df-pnf 10266  df-mnf 10267  df-ltxr 10269  df-sub 10458  df-neg 10459
This theorem is referenced by:  ltord2  10747  leord2  10748  eqord2  10749  possumd  10842  recgt0  11057  prodge0  11060  riotaneg  11192  negiso  11193  nn0negleid  11535  difgtsumgt  11536  nnnegz  11570  modsub12d  12919  monoord2  13024  discr1  13192  discr  13193  recj  14061  reneg  14062  imcj  14069  imneg  14070  abslt  14251  absle  14252  o1lo1  14465  o1lo12  14466  icco1  14468  rlimrege0  14507  lo1sub  14558  iseraltlem2  14610  infcvgaux1i  14786  absefib  15125  efieq1re  15126  moddvds  15191  bitscmp  15360  bitsinv1lem  15363  mulgnegnn  17750  cnsubrg  20006  xrhmeo  22944  pjthlem1  23406  ivth2  23422  ovolshft  23477  shftmbl  23504  volsup2  23571  volivth  23573  mbfmulc2lem  23611  mbfposr  23616  mbfposb  23617  ismbf3d  23618  mbfmulc2  23627  mbfinf  23629  mbfi1fseqlem4  23682  mbfi1fseqlem5  23683  mbfi1fseqlem6  23684  mbfi1flimlem  23686  itg2monolem1  23714  iblposlem  23755  iblre  23757  itgreval  23760  itgneg  23767  i1fibl  23771  itgitg1  23772  itgle  23773  ibladd  23784  itgaddlem2  23787  iblabslem  23791  itgmulc2lem2  23796  itgmulc2  23797  dvferm2lem  23946  dvferm2  23947  rolle  23950  dvivth  23970  lhop2  23975  dvfsumge  23982  dvfsumlem2  23987  dvfsum2  23994  coseq0negpitopi  24452  tanabsge  24455  tanord  24481  tanregt0  24482  abslogimle  24517  logcj  24549  argimgt0  24555  logdiv2  24560  logcnlem3  24587  dvloglem  24591  logccv  24606  abscxpbnd  24691  logreclem  24697  asinlem3a  24794  asinneg  24810  atanlogsublem  24839  atantan  24847  atans2  24855  birthdaylem3  24877  cxplim  24895  amgmlem  24913  emcllem7  24925  zetacvg  24938  eldmgm  24945  lgamgulmlem2  24953  lgsneg  25243  lgsdilem  25246  lgseisenlem1  25297  pntpbnd1  25472  pntibndlem2  25477  padicabvcxp  25518  ostth3  25524  axsegconlem9  26002  nvabs  27834  pjhthlem1  28557  xlt2addrd  29830  xrge0iifcnv  30286  xrge0iifiso  30288  xrge0iifhom  30290  dya2ub  30639  sgnmul  30911  signsply0  30935  fdvneggt  30985  fdvnegge  30987  climlec3  31924  poimirlem29  33749  itg2gt0cn  33776  ibladdnc  33778  itgaddnclem2  33780  iblabsnclem  33784  itgmulc2nclem2  33788  itgmulc2nc  33789  bddiblnc  33791  ftc1anclem5  33800  dvasin  33807  areacirclem1  33811  areacirclem4  33814  areacirclem5  33815  areacirc  33816  pellexlem6  37898  pell1234qrdich  37925  acongeq  38050  radcnvrat  39013  binomcxplemdvbinom  39052  binomcxplemnotnn0  39055  infnsuprnmpt  39962  neglt  39993  fperiodmul  40015  supsubc  40065  ltmulneg  40111  rexabslelem  40141  supminfrnmpt  40168  leneg2d  40172  leneg3d  40183  supminfxr  40190  climliminflimsupd  40534  liminfreuzlem  40535  liminfltlem  40537  stoweidlem1  40719  stoweidlem7  40725  stoweidlem13  40731  stoweidlem23  40741  stoweidlem34  40752  stoweidlem42  40760  stoweidlem47  40765  stirlinglem6  40797  stirlinglem10  40801  fourierdlem24  40849  fourierdlem39  40864  fourierdlem40  40865  fourierdlem43  40868  fourierdlem44  40869  fourierdlem46  40870  fourierdlem48  40872  fourierdlem49  40873  fourierdlem58  40882  fourierdlem62  40886  fourierdlem72  40896  fourierdlem78  40902  fourierdlem83  40907  fourierdlem85  40909  fourierdlem88  40912  fourierdlem92  40916  fourierdlem97  40921  fourierdlem103  40927  fourierdlem104  40928  fourierdlem109  40933  fourierdlem111  40935  fourierdlem112  40936  sqwvfoura  40946  etransclem23  40975  etransclem46  40998  hoicvr  41266  hoicvrrex  41274  smfinflem  41527  smfliminflem  41540  sigaradd  41559  proththd  42039  dignn0flhalflem1  42917  amgmwlem  43059
  Copyright terms: Public domain W3C validator