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

Theorem negcld 9923
Description: Closure law for negative. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
negidd.1  |-  ( ph  ->  A  e.  CC )
Assertion
Ref Expression
negcld  |-  ( ph  -> 
-u A  e.  CC )

Proof of Theorem negcld
StepHypRef Expression
1 negidd.1 . 2  |-  ( ph  ->  A  e.  CC )
2 negcl 9825 . 2  |-  ( A  e.  CC  ->  -u A  e.  CC )
31, 2syl 16 1  |-  ( ph  -> 
-u A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1804   CCcc 9493   -ucneg 9811
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-resscn 9552  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-mulcom 9559  ax-addass 9560  ax-mulass 9561  ax-distr 9562  ax-i2m1 9563  ax-1ne0 9564  ax-1rid 9565  ax-rnegex 9566  ax-rrecex 9567  ax-cnre 9568  ax-pre-lttri 9569  ax-pre-lttrn 9570  ax-pre-ltadd 9571
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-reu 2800  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-po 4790  df-so 4791  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-riota 6242  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-er 7313  df-en 7519  df-dom 7520  df-sdom 7521  df-pnf 9633  df-mnf 9634  df-ltxr 9636  df-sub 9812  df-neg 9813
This theorem is referenced by:  negcon1ad  9931  recextlem1  10186  xov1plusxeqvd  11677  ceim1l  11956  modnegd  12024  expaddzlem  12191  cjreb  12938  sqrtneg  13083  max0add  13125  iseraltlem2  13487  iseraltlem3  13488  fsumsub  13585  telfsumo2  13599  incexc  13631  incexc2  13632  efi4p  13854  oexpneg  14031  bitscmp  14070  bitsf1  14078  pcadd2  14391  gznegcl  14435  mulgdirlem  16145  mulgdir  16146  znunit  18580  cphsqrtcl2  21611  pjthlem1  21830  mbfsub  22047  iblcnlem1  22172  itgcnlem  22174  iblneg  22187  itgneg  22188  iblsub  22206  itgsub  22210  ditgcl  22240  dvrec  22336  dvmptsub  22348  dvsincos  22360  rolle  22369  vieta1lem2  22685  vieta1  22686  sinmpi  22858  cosmpi  22859  sinppi  22860  cosppi  22861  tanabsge  22877  efeq1  22894  tanord  22903  logtayl  23019  logtayl2  23021  logccv  23022  cxpneg  23040  cxpmul2z  23050  cosangneg2d  23117  logreclem  23128  isosctrlem2  23131  isosctrlem3  23132  angpieqvdlem  23137  quad2  23148  dcubic1lem  23152  dcubic2  23153  dcubic  23155  mcubic  23156  dquartlem1  23160  dquartlem2  23161  dquart  23162  quartlem1  23166  quartlem2  23167  quartlem3  23168  quartlem4  23169  quart  23170  asinlem  23177  asinlem2  23178  asinneg  23195  sinasin  23198  cosasin  23213  atandmneg  23215  tanatan  23228  atandmtan  23229  atantan  23232  atantayl  23246  ftalem4  23327  ftalem5  23328  ftalem7  23330  basellem5  23336  chpdifbndlem1  23716  padicabvcxp  23795  brbtwn2  24186  gxsuc  25252  ipasslem2  25725  pjhthlem1  26287  mul2lt0rlt0  27543  divnumden2  27587  archirngz  27711  zetacvg  28535  dmgmaddnn0  28547  lgamgulmlem2  28550  lgamgulmlem4  28552  lgambdd  28557  lgamucov  28558  fallrisefac  29123  binomrisefac  29140  dvtan  30041  itg2addnclem3  30044  iblsubnc  30052  itgsubnc  30053  itgmulc2nc  30059  ftc1anclem5  30070  ftc1anclem8  30073  dvasin  30079  areacirclem1  30083  pell1234qrreccl  30766  pell14qrdich  30781  rmxyneg  30832  acongsym  30890  jm2.26a  30918  jm2.26lem3  30919  expgrowth  31216  fzisoeu  31454  fperiodmul  31458  m1expeven  31539  isumneg  31562  climneg  31570  neglimc  31607  sublimc  31612  reclimc  31613  dvcosre  31660  dvrecg  31661  dvmptdiv  31668  dvcosax  31677  itgsin0pilem1  31702  itgsinexplem1  31706  itgsincmulx  31727  stoweidlem13  31749  stirlinglem5  31814  dirkertrigeqlem3  31836  fourierdlem30  31873  fourierdlem39  31882  fourierdlem40  31883  fourierdlem41  31884  fourierdlem43  31886  fourierdlem47  31890  fourierdlem48  31891  fourierdlem49  31892  fourierdlem73  31916  fourierdlem78  31921  fourierdlem92  31935  fourierdlem101  31944  fourierdlem103  31946  fourierdlem111  31954  sqwvfoura  31965  fouriersw  31968  etransclem17  31988  etransclem18  31989  etransclem23  31994  etransclem46  32017  sigarms  32027  sigaradd  32037  2zrngagrp  32576  altgsumbc  32809  sineq0ALT  33605
  Copyright terms: Public domain W3C validator