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

Theorem negcld 9693
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 9597 . 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 1755   CCcc 9267   -ucneg 9583
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-resscn 9326  ax-1cn 9327  ax-icn 9328  ax-addcl 9329  ax-addrcl 9330  ax-mulcl 9331  ax-mulrcl 9332  ax-mulcom 9333  ax-addass 9334  ax-mulass 9335  ax-distr 9336  ax-i2m1 9337  ax-1ne0 9338  ax-1rid 9339  ax-rnegex 9340  ax-rrecex 9341  ax-cnre 9342  ax-pre-lttri 9343  ax-pre-lttrn 9344  ax-pre-ltadd 9345
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-nel 2599  df-ral 2710  df-rex 2711  df-reu 2712  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-mpt 4340  df-id 4623  df-po 4628  df-so 4629  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-riota 6039  df-ov 6083  df-oprab 6084  df-mpt2 6085  df-er 7089  df-en 7299  df-dom 7300  df-sdom 7301  df-pnf 9407  df-mnf 9408  df-ltxr 9410  df-sub 9584  df-neg 9585
This theorem is referenced by:  negcon1ad  9701  recextlem1  9953  xov1plusxeqvd  11417  ceim1l  11669  modnegd  11737  expaddzlem  11890  cjreb  12595  sqrneg  12740  max0add  12782  iseraltlem2  13143  iseraltlem3  13144  fsumsub  13237  fsumtscopo2  13248  incexc  13282  incexc2  13283  efi4p  13403  oexpneg  13577  bitscmp  13616  bitsf1  13624  pcadd2  13934  gznegcl  13978  mulgdirlem  15630  mulgdir  15631  znunit  17837  cphsqrcl2  20546  pjthlem1  20765  mbfsub  20981  iblcnlem1  21106  itgcnlem  21108  iblneg  21121  itgneg  21122  iblsub  21140  itgsub  21144  ditgcl  21174  dvrec  21270  dvmptsub  21282  dvsincos  21294  rolle  21303  vieta1lem2  21661  vieta1  21662  sinmpi  21833  cosmpi  21834  sinppi  21835  cosppi  21836  tanabsge  21852  efeq1  21869  tanord  21878  logtayl  21989  logtayl2  21991  logccv  21992  cxpneg  22010  cxpmul2z  22020  cosangneg2d  22087  logreclem  22098  isosctrlem2  22101  isosctrlem3  22102  angpieqvdlem  22107  quad2  22118  dcubic1lem  22122  dcubic2  22123  dcubic  22125  mcubic  22126  dquartlem1  22130  dquartlem2  22131  dquart  22132  quartlem1  22136  quartlem2  22137  quartlem3  22138  quartlem4  22139  quart  22140  asinlem  22147  asinlem2  22148  asinneg  22165  sinasin  22168  cosasin  22183  atandmneg  22185  tanatan  22198  atandmtan  22199  atantan  22202  atantayl  22216  ftalem4  22297  ftalem5  22298  ftalem7  22300  basellem5  22306  chpdifbndlem1  22686  padicabvcxp  22765  brbtwn2  22973  gxsuc  23581  ipasslem2  24054  pjhthlem1  24616  mul2lt0rlt0  25862  divnumden2  25909  archirngz  26029  zetacvg  26848  dmgmaddnn0  26860  lgamgulmlem2  26863  lgamgulmlem4  26865  lgambdd  26870  lgamucov  26871  fallrisefac  27374  binomrisefac  27391  dvtan  28283  itg2addnclem3  28286  iblsubnc  28294  itgsubnc  28295  itgmulc2nc  28301  ftc1anclem5  28312  ftc1anclem8  28315  dvasin  28321  areacirclem1  28325  pell1234qrreccl  29037  pell14qrdich  29052  rmxyneg  29103  acongsym  29161  jm2.26a  29191  jm2.26lem3  29192  expgrowth  29451  m1expeven  29615  isumneg  29618  climneg  29626  dvcosre  29631  itgsin0pilem1  29633  itgsinexplem1  29637  stoweidlem13  29651  stirlinglem5  29716  sigarms  29735  sigaradd  29745  sineq0ALT  31372
  Copyright terms: Public domain W3C validator