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

Theorem negcld 9974
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 9876 . 2  |-  ( A  e.  CC  ->  -u A  e.  CC )
31, 2syl 17 1  |-  ( ph  -> 
-u A  e.  CC )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1868   CCcc 9538   -ucneg 9862
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657  ax-un 6594  ax-resscn 9597  ax-1cn 9598  ax-icn 9599  ax-addcl 9600  ax-addrcl 9601  ax-mulcl 9602  ax-mulrcl 9603  ax-mulcom 9604  ax-addass 9605  ax-mulass 9606  ax-distr 9607  ax-i2m1 9608  ax-1ne0 9609  ax-1rid 9610  ax-rnegex 9611  ax-rrecex 9612  ax-cnre 9613  ax-pre-lttri 9614  ax-pre-lttrn 9615  ax-pre-ltadd 9616
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-reu 2782  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4765  df-po 4771  df-so 4772  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-iota 5562  df-fun 5600  df-fn 5601  df-f 5602  df-f1 5603  df-fo 5604  df-f1o 5605  df-fv 5606  df-riota 6264  df-ov 6305  df-oprab 6306  df-mpt2 6307  df-er 7368  df-en 7575  df-dom 7576  df-sdom 7577  df-pnf 9678  df-mnf 9679  df-ltxr 9681  df-sub 9863  df-neg 9864
This theorem is referenced by:  negcon1ad  9982  recextlem1  10243  mul2lt0rlt0  11399  xov1plusxeqvd  11779  ceim1l  12074  modnegd  12145  expaddzlem  12315  cjreb  13175  sqrtneg  13320  max0add  13362  iseraltlem2  13737  iseraltlem3  13738  fsumsub  13837  telfsumo2  13851  incexc  13883  incexc2  13884  fallrisefac  14066  binomrisefac  14083  efi4p  14179  oexpneg  14356  bitscmp  14400  bitsf1  14408  pcadd2  14823  gznegcl  14867  mulgdirlem  16770  mulgdir  16771  znunit  19121  cphsqrtcl2  22151  pjthlem1  22378  mbfsub  22605  iblcnlem1  22732  itgcnlem  22734  iblneg  22747  itgneg  22748  iblsub  22766  itgsub  22770  ditgcl  22800  dvrec  22896  dvmptsub  22908  dvsincos  22920  rolle  22929  vieta1lem2  23251  vieta1  23252  sinmpi  23429  cosmpi  23430  sinppi  23431  cosppi  23432  tanabsge  23448  efeq1  23465  tanord  23474  logtayl  23592  logtayl2  23594  logccv  23595  cxpneg  23613  cxpmul2z  23623  logreclem  23686  cosangneg2d  23723  isosctrlem2  23735  isosctrlem3  23736  angpieqvdlem  23741  quad2  23752  dcubic1lem  23756  dcubic2  23757  dcubic  23759  mcubic  23760  dquartlem1  23764  dquartlem2  23765  dquart  23766  quartlem1  23770  quartlem2  23771  quartlem3  23772  quartlem4  23773  quart  23774  asinlem  23781  asinlem2  23782  asinneg  23799  sinasin  23802  cosasin  23817  atandmneg  23819  tanatan  23832  atandmtan  23833  atantan  23836  atantayl  23850  zetacvg  23927  dmgmaddnn0  23939  lgamgulmlem2  23942  lgamgulmlem4  23944  lgambdd  23949  lgamucov  23950  ftalem4  23987  ftalem5  23988  ftalem4OLD  23989  ftalem5OLD  23990  ftalem7  23992  basellem5  23998  chpdifbndlem1  24378  padicabvcxp  24457  brbtwn2  24922  gxsuc  25986  ipasslem2  26459  pjhthlem1  27030  divnumden2  28376  archirngz  28501  madjusmdetlem4  28652  poimirlem29  31883  dvtan  31906  itg2addnclem3  31909  iblsubnc  31917  itgsubnc  31918  itgmulc2nc  31924  ftc1anclem5  31935  ftc1anclem8  31938  dvasin  31942  areacirclem1  31946  pell1234qrreccl  35620  pell14qrdich  35635  rmxyneg  35688  acongsym  35746  jm2.26a  35775  jm2.26lem3  35776  expgrowth  36542  binomcxplemdvbinom  36560  binomcxplemnotnn0  36563  sineq0ALT  37195  fzisoeu  37360  fperiodmul  37364  m1expevenOLD  37490  isumneg  37500  climneg  37509  neglimc  37548  sublimc  37553  reclimc  37554  dvcosre  37601  dvrecg  37602  dvmptdiv  37609  dvcosax  37618  itgsin0pilem1  37646  itgsinexplem1  37650  itgsincmulx  37671  stoweidlem13  37693  stirlinglem5  37760  dirkertrigeqlem3  37782  fourierdlem30  37819  fourierdlem39  37829  fourierdlem40  37830  fourierdlem41  37831  fourierdlem43  37834  fourierdlem47  37837  fourierdlem48  37838  fourierdlem49  37839  fourierdlem73  37863  fourierdlem78  37868  fourierdlem92  37882  fourierdlem101  37891  fourierdlem103  37893  fourierdlem111  37901  sqwvfoura  37912  fouriersw  37915  etransclem17  37936  etransclem18  37937  etransclem23  37942  etransclem46  37965  sigarms  38178  sigaradd  38188  oexpnegALTV  38518  oexpnegnz  38519  2zrngagrp  39215  altgsumbc  39407  dignn0flhalflem1  39700
  Copyright terms: Public domain W3C validator