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

Theorem negcld 9234
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 9142 . 2  |-  ( A  e.  CC  ->  -u A  e.  CC )
31, 2syl 15 1  |-  ( ph  -> 
-u A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1710   CCcc 8825   -ucneg 9128
This theorem is referenced by:  negcon1ad  9242  recextlem1  9488  xov1plusxeqvd  10872  ceim1l  11049  modnegd  11096  expaddzlem  11238  cjreb  11704  sqrneg  11849  max0add  11891  iseraltlem2  12252  iseraltlem3  12253  fsumsub  12347  fsumtscopo2  12358  incexc  12393  incexc2  12394  efi4p  12514  oexpneg  12687  bitscmp  12726  bitsf1  12734  pcadd2  13035  gznegcl  13079  mulgdirlem  14690  mulgdir  14691  znunit  16623  cphsqrcl2  18726  pjthlem1  18905  mbfsub  19121  iblcnlem1  19246  itgcnlem  19248  iblneg  19261  itgneg  19262  iblsub  19280  itgsub  19284  ditgcl  19312  dvrec  19408  dvmptsub  19420  dvsincos  19432  rolle  19441  vieta1lem2  19795  vieta1  19796  sinmpi  19962  cosmpi  19963  sinppi  19964  cosppi  19965  tanabsge  19981  efeq1  19998  tanord  20007  logtayl  20118  logtayl2  20120  logccv  20121  cxpneg  20139  cxpmul2z  20149  cosangneg2d  20216  logreclem  20227  isosctrlem2  20230  isosctrlem3  20231  angpieqvdlem  20236  quad2  20246  dcubic1lem  20250  dcubic2  20251  dcubic  20253  mcubic  20254  dquartlem1  20258  dquartlem2  20259  dquart  20260  quartlem1  20264  quartlem2  20265  quartlem3  20266  quartlem4  20267  quart  20268  asinlem  20275  asinlem2  20276  asinneg  20293  sinasin  20296  cosasin  20311  atandmneg  20313  tanatan  20326  atandmtan  20327  atantan  20330  atantayl  20344  ftalem4  20425  ftalem5  20426  ftalem7  20428  basellem5  20434  chpdifbndlem1  20814  padicabvcxp  20893  gxsuc  21051  ipasslem2  21524  pjhthlem1  22084  divnumden2  23365  zetacvg  24048  dmgmaddnn0  24060  lgamgulmlem2  24063  lgamgulmlem4  24065  lgambdd  24070  lgamucov  24071  brbtwn2  25092  itg2addnc  25494  iblsubnc  25501  itgsubnc  25502  itgmulc2nc  25508  dvreasin  25515  areacirclem2  25517  pell1234qrreccl  26262  pell14qrdich  26277  rmxyneg  26328  acongsym  26386  jm2.26a  26416  jm2.26lem3  26417  expgrowth  26875  m1expeven  27048  isumneg  27051  climneg  27059  dvcosre  27064  itgsin0pilem1  27067  itgsinexplem1  27071  stirlinglem5  27150  sigarms  27169  sigaradd  27179
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4222  ax-nul 4230  ax-pow 4269  ax-pr 4295  ax-un 4594  ax-resscn 8884  ax-1cn 8885  ax-icn 8886  ax-addcl 8887  ax-addrcl 8888  ax-mulcl 8889  ax-mulrcl 8890  ax-mulcom 8891  ax-addass 8892  ax-mulass 8893  ax-distr 8894  ax-i2m1 8895  ax-1ne0 8896  ax-1rid 8897  ax-rnegex 8898  ax-rrecex 8899  ax-cnre 8900  ax-pre-lttri 8901  ax-pre-lttrn 8902  ax-pre-ltadd 8903
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-nel 2524  df-ral 2624  df-rex 2625  df-reu 2626  df-rab 2628  df-v 2866  df-sbc 3068  df-csb 3158  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3909  df-br 4105  df-opab 4159  df-mpt 4160  df-id 4391  df-po 4396  df-so 4397  df-xp 4777  df-rel 4778  df-cnv 4779  df-co 4780  df-dm 4781  df-rn 4782  df-res 4783  df-ima 4784  df-iota 5301  df-fun 5339  df-fn 5340  df-f 5341  df-f1 5342  df-fo 5343  df-f1o 5344  df-fv 5345  df-ov 5948  df-oprab 5949  df-mpt2 5950  df-riota 6391  df-er 6747  df-en 6952  df-dom 6953  df-sdom 6954  df-pnf 8959  df-mnf 8960  df-ltxr 8962  df-sub 9129  df-neg 9130
  Copyright terms: Public domain W3C validator