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

Theorem renegcld 11055
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 10937 . 2 (𝐴 ∈ ℝ → -𝐴 ∈ ℝ)
31, 2syl 17 1 (𝜑 → -𝐴 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  cr 10524  -cneg 10859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-po 5467  df-so 5468  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-er 8278  df-en 8498  df-dom 8499  df-sdom 8500  df-pnf 10665  df-mnf 10666  df-ltxr 10668  df-sub 10860  df-neg 10861
This theorem is referenced by:  ltord2  11157  leord2  11158  eqord2  11159  possumd  11253  recgt0  11474  riotaneg  11608  negiso  11609  nn0negleid  11937  difgtsumgt  11938  nnnegz  11972  prodge0rd  12484  modsub12d  13284  monoord2  13389  discr1  13588  discr  13589  recj  14471  reneg  14472  imcj  14479  imneg  14480  abslt  14662  absle  14663  o1lo1  14882  o1lo12  14883  icco1  14885  rlimrege0  14924  lo1sub  14975  iseraltlem2  15027  infcvgaux1i  15200  absefib  15539  efieq1re  15540  moddvds  15606  bitscmp  15775  bitsinv1lem  15778  mulgnegnn  18176  cnsubrg  20533  xrhmeo  23477  pjthlem1  23967  ivth2  23983  ovolshft  24039  shftmbl  24066  volsup2  24133  volivth  24135  mbfmulc2lem  24175  mbfposr  24180  mbfposb  24181  ismbf3d  24182  mbfmulc2  24191  mbfinf  24193  mbfi1fseqlem4  24246  mbfi1fseqlem5  24247  mbfi1fseqlem6  24248  mbfi1flimlem  24250  itg2monolem1  24278  iblposlem  24319  iblre  24321  itgreval  24324  itgneg  24331  i1fibl  24335  itgitg1  24336  itgle  24337  ibladd  24348  itgaddlem2  24351  iblabslem  24355  itgmulc2lem2  24360  itgmulc2  24361  dvferm2lem  24510  dvferm2  24511  rolle  24514  dvivth  24534  lhop2  24539  dvfsumge  24546  dvfsumlem2  24551  dvfsum2  24558  coseq0negpitopi  25016  tanabsge  25019  tanord  25049  tanregt0  25050  abslogimle  25084  logcj  25116  argimgt0  25122  logdiv2  25127  logcnlem3  25154  logccv  25173  abscxpbnd  25261  logreclem  25267  asinlem3a  25375  asinneg  25391  atanlogsublem  25420  atantan  25428  atans2  25436  birthdaylem3  25458  cxplim  25476  amgmlem  25494  emcllem7  25506  zetacvg  25519  eldmgm  25526  lgamgulmlem2  25534  lgsneg  25824  lgsdilem  25827  lgseisenlem1  25878  pntpbnd1  26089  pntibndlem2  26094  padicabvcxp  26135  ostth3  26141  axsegconlem9  26638  nvabs  28376  pjhthlem1  29095  xlt2addrd  30408  ccfldextdgrr  30956  xrge0iifcnv  31075  xrge0iifiso  31077  xrge0iifhom  31079  dya2ub  31427  sgnmul  31699  signsply0  31720  fdvneggt  31770  fdvnegge  31772  climlec3  32862  poimirlem29  34802  itg2gt0cn  34828  ibladdnc  34830  itgaddnclem2  34832  iblabsnclem  34836  itgmulc2nclem2  34840  itgmulc2nc  34841  bddiblnc  34843  ftc1anclem5  34852  dvasin  34859  areacirclem1  34863  areacirclem4  34866  areacirclem5  34867  areacirc  34868  oexpreposd  39057  3cubeslem4  39164  pellexlem6  39309  pell1234qrdich  39336  acongeq  39458  radcnvrat  40523  binomcxplemdvbinom  40562  binomcxplemnotnn0  40565  infnsuprnmpt  41398  neglt  41426  fperiodmul  41447  supsubc  41497  ltmulneg  41540  rexabslelem  41568  supminfrnmpt  41595  leneg2d  41599  leneg3d  41609  supminfxr  41616  climliminflimsupd  41958  liminfreuzlem  41959  liminfltlem  41961  stoweidlem1  42163  stoweidlem7  42169  stoweidlem13  42175  stoweidlem23  42185  stoweidlem34  42196  stoweidlem42  42204  stoweidlem47  42209  stirlinglem6  42241  stirlinglem10  42245  fourierdlem24  42293  fourierdlem39  42308  fourierdlem40  42309  fourierdlem43  42312  fourierdlem44  42313  fourierdlem46  42314  fourierdlem48  42316  fourierdlem49  42317  fourierdlem58  42326  fourierdlem62  42330  fourierdlem72  42340  fourierdlem78  42346  fourierdlem83  42351  fourierdlem85  42353  fourierdlem88  42356  fourierdlem92  42360  fourierdlem97  42365  fourierdlem103  42371  fourierdlem104  42372  fourierdlem109  42377  fourierdlem111  42379  fourierdlem112  42380  sqwvfoura  42390  etransclem23  42419  etransclem46  42442  hoicvr  42707  hoicvrrex  42715  smfinflem  42968  smfliminflem  42981  sigaradd  43000  sqrtnegnre  43384  proththd  43656  requad01  43663  requad1  43664  requad2  43665  dignn0flhalflem1  44603  eenglngeehlnmlem1  44652  eenglngeehlnmlem2  44653  line2ylem  44666  itscnhlc0yqe  44674  itsclquadb  44691  itscnhlinecirc02p  44700  amgmwlem  44831
  Copyright terms: Public domain W3C validator