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

Theorem renegcld 9767
Description: Closure law for negative of reals. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
renegcld.1  |-  ( ph  ->  A  e.  RR )
Assertion
Ref Expression
renegcld  |-  ( ph  -> 
-u A  e.  RR )

Proof of Theorem renegcld
StepHypRef Expression
1 renegcld.1 . 2  |-  ( ph  ->  A  e.  RR )
2 renegcl 9664 . 2  |-  ( A  e.  RR  ->  -u A  e.  RR )
31, 2syl 16 1  |-  ( ph  -> 
-u A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   RRcr 9273   -ucneg 9588
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2715  df-rex 2716  df-reu 2717  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-po 4636  df-so 4637  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-riota 6047  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-er 7093  df-en 7303  df-dom 7304  df-sdom 7305  df-pnf 9412  df-mnf 9413  df-ltxr 9415  df-sub 9589  df-neg 9590
This theorem is referenced by:  ltord2  9861  leord2  9862  eqord2  9863  recgt0  10165  prodge0  10168  riotaneg  10297  negiso  10298  infmrcl  10301  nnnegz  10641  modsub12d  11748  monoord2  11829  discr1  11992  discr  11993  recj  12605  reneg  12606  imcj  12613  imneg  12614  abslt  12794  absle  12795  o1lo1  13007  o1lo12  13008  icco1  13010  rlimrege0  13049  lo1sub  13100  iseraltlem2  13152  infcvgaux1i  13311  absefib  13474  efieq1re  13475  moddvds  13534  bitscmp  13626  bitsinv1lem  13629  mulgnegnn  15628  cnsubrg  17848  xrhmeo  20493  pjthlem1  20899  ivth2  20914  ovolshft  20969  shftmbl  20995  volsup2  21060  volivth  21062  mbfmulc2lem  21100  mbfposr  21105  mbfposb  21106  ismbf3d  21107  mbfmulc2  21116  mbfinf  21118  mbfi1fseqlem4  21171  mbfi1fseqlem5  21172  mbfi1fseqlem6  21173  mbfi1flimlem  21175  itg2monolem1  21203  iblposlem  21244  iblre  21246  itgreval  21249  itgneg  21256  i1fibl  21260  itgitg1  21261  itgle  21262  ibladd  21273  itgaddlem2  21276  iblabslem  21280  itgmulc2lem2  21285  itgmulc2  21286  dvferm2lem  21433  dvferm2  21434  rolle  21437  dvivth  21457  lhop2  21462  dvfsumge  21469  dvfsumlem2  21474  dvfsum2  21481  coseq0negpitopi  21940  tanabsge  21943  tanord  21969  tanregt0  21970  abslogimle  22000  logcj  22030  argimgt0  22036  logdiv2  22041  logcnlem3  22064  dvloglem  22068  logccv  22083  abscxpbnd  22166  logreclem  22189  asinlem3a  22240  asinneg  22256  atanlogsublem  22285  atantan  22293  atans2  22301  birthdaylem3  22322  cxplim  22340  amgmlem  22358  emcllem7  22370  lgsneg  22633  lgsdilem  22636  lgseisenlem1  22663  pntpbnd1  22810  pntibndlem2  22815  padicabvcxp  22856  ostth3  22862  axsegconlem9  23122  nvabs  24012  pjhthlem1  24745  xlt2addrd  26002  xrge0iifcnv  26315  xrge0iifiso  26317  xrge0iifhom  26319  dya2ub  26637  sgnmul  26877  signsply0  26904  zetacvg  26953  eldmgm  26960  lgamgulmlem2  26968  possumd  27347  climlec3  27352  itg2gt0cn  28400  ibladdnc  28402  itgaddnclem2  28404  iblabsnclem  28408  itgmulc2nclem2  28412  itgmulc2nc  28413  bddiblnc  28415  ftc1anclem5  28424  dvasin  28433  areacirclem1  28437  areacirclem4  28440  areacirclem5  28441  areacirc  28442  pellexlem6  29128  pell1234qrdich  29155  acongeq  29279  stoweidlem1  29749  stoweidlem7  29755  stoweidlem13  29761  stoweidlem23  29771  stoweidlem34  29782  stoweidlem42  29790  stoweidlem47  29795  stirlinglem6  29827  stirlinglem10  29831  sigaradd  29855
  Copyright terms: Public domain W3C validator