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

Theorem renegcld 10034
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 9923 . 2  |-  ( A  e.  RR  ->  -u A  e.  RR )
31, 2syl 17 1  |-  ( ph  -> 
-u A  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1890   RRcr 9524   -ucneg 9847
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-8 1892  ax-9 1899  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091  ax-ext 2431  ax-sep 4496  ax-nul 4505  ax-pow 4553  ax-pr 4611  ax-un 6570  ax-resscn 9582  ax-1cn 9583  ax-icn 9584  ax-addcl 9585  ax-addrcl 9586  ax-mulcl 9587  ax-mulrcl 9588  ax-mulcom 9589  ax-addass 9590  ax-mulass 9591  ax-distr 9592  ax-i2m1 9593  ax-1ne0 9594  ax-1rid 9595  ax-rnegex 9596  ax-rrecex 9597  ax-cnre 9598  ax-pre-lttri 9599  ax-pre-lttrn 9600  ax-pre-ltadd 9601
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1450  df-ex 1667  df-nf 1671  df-sb 1801  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rab 2745  df-v 3014  df-sbc 3235  df-csb 3331  df-dif 3374  df-un 3376  df-in 3378  df-ss 3385  df-nul 3699  df-if 3849  df-pw 3920  df-sn 3936  df-pr 3938  df-op 3942  df-uni 4168  df-br 4374  df-opab 4433  df-mpt 4434  df-id 4726  df-po 4732  df-so 4733  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5524  df-fun 5562  df-fn 5563  df-f 5564  df-f1 5565  df-fo 5566  df-f1o 5567  df-fv 5568  df-riota 6237  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-er 7349  df-en 7556  df-dom 7557  df-sdom 7558  df-pnf 9663  df-mnf 9664  df-ltxr 9666  df-sub 9848  df-neg 9849
This theorem is referenced by:  ltord2  10131  leord2  10132  eqord2  10133  recgt0  10437  prodge0  10440  riotaneg  10574  negiso  10575  infmrclOLD  10581  nnnegz  10929  modsub12d  12140  monoord2  12237  discr1  12401  discr  12402  recj  13197  reneg  13198  imcj  13205  imneg  13206  abslt  13387  absle  13388  o1lo1  13611  o1lo12  13612  icco1  13614  rlimrege0  13653  lo1sub  13704  iseraltlem2  13759  infcvgaux1i  13925  absefib  14262  efieq1re  14263  moddvds  14322  bitscmp  14422  bitsinv1lem  14425  mulgnegnn  16778  cnsubrg  19038  xrhmeo  21984  pjthlem1  22401  ivth2  22416  ovolshft  22474  shftmbl  22502  volsup2  22574  volivth  22576  mbfmulc2lem  22614  mbfposr  22619  mbfposb  22620  ismbf3d  22621  mbfmulc2  22630  mbfinf  22632  mbfinfOLD  22633  mbfi1fseqlem4  22687  mbfi1fseqlem5  22688  mbfi1fseqlem6  22689  mbfi1flimlem  22691  itg2monolem1  22719  iblposlem  22760  iblre  22762  itgreval  22765  itgneg  22772  i1fibl  22776  itgitg1  22777  itgle  22778  ibladd  22789  itgaddlem2  22792  iblabslem  22796  itgmulc2lem2  22801  itgmulc2  22802  dvferm2lem  22949  dvferm2  22950  rolle  22953  dvivth  22973  lhop2  22978  dvfsumge  22985  dvfsumlem2  22990  dvfsum2  22997  coseq0negpitopi  23469  tanabsge  23472  tanord  23498  tanregt0  23499  abslogimle  23534  logcj  23566  argimgt0  23572  logdiv2  23577  logcnlem3  23600  dvloglem  23604  logccv  23619  abscxpbnd  23704  logreclem  23710  asinlem3a  23807  asinneg  23823  atanlogsublem  23852  atantan  23860  atans2  23868  birthdaylem3  23890  cxplim  23908  amgmlem  23926  emcllem7  23938  zetacvg  23951  eldmgm  23958  lgamgulmlem2  23966  lgsneg  24258  lgsdilem  24261  lgseisenlem1  24288  pntpbnd1  24435  pntibndlem2  24440  padicabvcxp  24481  ostth3  24487  axsegconlem9  24966  nvabs  26313  pjhthlem1  27055  xlt2addrd  28345  xrge0iifcnv  28745  xrge0iifiso  28747  xrge0iifhom  28749  dya2ub  29097  sgnmul  29418  signsply0  29445  possumd  30371  climlec3  30374  poimirlem29  31970  itg2gt0cn  31998  ibladdnc  32000  itgaddnclem2  32002  iblabsnclem  32006  itgmulc2nclem2  32010  itgmulc2nc  32011  bddiblnc  32013  ftc1anclem5  32022  dvasin  32029  areacirclem1  32033  areacirclem4  32036  areacirclem5  32037  areacirc  32038  pellexlem6  35679  pell1234qrdich  35708  acongeq  35834  radcnvrat  36663  binomcxplemdvbinom  36702  binomcxplemnotnn0  36705  neglt  37524  fperiodmul  37552  supsubc  37606  stoweidlem1  37917  stoweidlem7  37923  stoweidlem13  37929  stoweidlem23  37939  stoweidlem34  37951  stoweidlem42  37959  stoweidlem47  37964  stirlinglem6  37997  stirlinglem10  38001  fourierdlem24  38049  fourierdlem39  38065  fourierdlem40  38066  fourierdlem43  38070  fourierdlem44  38071  fourierdlem46  38072  fourierdlem48  38074  fourierdlem49  38075  fourierdlem58  38084  fourierdlem62  38088  fourierdlem72  38098  fourierdlem78  38104  fourierdlem83  38109  fourierdlem85  38111  fourierdlem88  38114  fourierdlem92  38118  fourierdlem97  38123  fourierdlem103  38129  fourierdlem104  38130  fourierdlem109  38135  fourierdlem111  38137  fourierdlem112  38138  sqwvfoura  38148  etransclem23  38178  etransclem46  38201  hoicvr  38432  hoicvrrex  38440  sigaradd  38565  proththd  39004  dignn0flhalflem1  40750
  Copyright terms: Public domain W3C validator