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

Theorem negcl 9307
Description: Closure law for negative. (Contributed by NM, 6-Aug-2003.)
Assertion
Ref Expression
negcl  |-  ( A  e.  CC  ->  -u A  e.  CC )

Proof of Theorem negcl
StepHypRef Expression
1 df-neg 9295 . 2  |-  -u A  =  ( 0  -  A )
2 0cn 9085 . . 3  |-  0  e.  CC
3 subcl 9306 . . 3  |-  ( ( 0  e.  CC  /\  A  e.  CC )  ->  ( 0  -  A
)  e.  CC )
42, 3mpan 653 . 2  |-  ( A  e.  CC  ->  (
0  -  A )  e.  CC )
51, 4syl5eqel 2521 1  |-  ( A  e.  CC  ->  -u A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726  (class class class)co 6082   CCcc 8989   0cc0 8991    - cmin 9292   -ucneg 9293
This theorem is referenced by:  negcon1  9354  negdi  9359  negdi2  9360  negsubdi2  9361  neg2sub  9362  negcli  9369  negcld  9399  mulneg2  9472  mul2neg  9474  mulsub  9477  divneg  9710  divsubdir  9711  divsubdiv  9731  eqneg  9735  div2neg  9738  divneg2  9739  zeo  10356  sqneg  11443  binom2sub  11499  shftval4  11893  shftcan1  11899  shftcan2  11900  crim  11921  resub  11933  imsub  11941  cjneg  11953  cjsub  11955  absneg  12083  abs2dif2  12138  sqreulem  12164  sqreu  12165  subcn2  12389  efcan  12698  efne0  12699  efneg  12700  efsub  12702  sinneg  12748  cosneg  12749  tanneg  12750  efmival  12755  sinhval  12756  coshval  12757  sinsub  12770  cossub  12771  sincossq  12778  cnaddablx  15482  cnaddabl  15483  cncrng  16723  cnfldneg  16728  plyremlem  20222  reeff1o  20364  sin2pim  20394  cos2pim  20395  cxpsub  20574  cxpsqr  20595  logrec  20662  asinlem3  20712  asinneg  20727  acosneg  20728  sinasin  20730  asinsin  20733  cosasin  20745  atantan  20764  cnaddablo  21939  addinv  21941  vcsubdir  22036  hvsubdistr2  22553  spanunsni  23082  risefallfac  25341  fallrisefac  25342  fallfac0  25345  binomrisefac  25359  ltflcei  26240  sinhpcosh  28484
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418  ax-sep 4331  ax-nul 4339  ax-pow 4378  ax-pr 4404  ax-un 4702  ax-resscn 9048  ax-1cn 9049  ax-icn 9050  ax-addcl 9051  ax-addrcl 9052  ax-mulcl 9053  ax-mulrcl 9054  ax-mulcom 9055  ax-addass 9056  ax-mulass 9057  ax-distr 9058  ax-i2m1 9059  ax-1ne0 9060  ax-1rid 9061  ax-rnegex 9062  ax-rrecex 9063  ax-cnre 9064  ax-pre-lttri 9065  ax-pre-lttrn 9066  ax-pre-ltadd 9067
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2286  df-mo 2287  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-nel 2603  df-ral 2711  df-rex 2712  df-reu 2713  df-rab 2715  df-v 2959  df-sbc 3163  df-csb 3253  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3630  df-if 3741  df-pw 3802  df-sn 3821  df-pr 3822  df-op 3824  df-uni 4017  df-br 4214  df-opab 4268  df-mpt 4269  df-id 4499  df-po 4504  df-so 4505  df-xp 4885  df-rel 4886  df-cnv 4887  df-co 4888  df-dm 4889  df-rn 4890  df-res 4891  df-ima 4892  df-iota 5419  df-fun 5457  df-fn 5458  df-f 5459  df-f1 5460  df-fo 5461  df-f1o 5462  df-fv 5463  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-riota 6550  df-er 6906  df-en 7111  df-dom 7112  df-sdom 7113  df-pnf 9123  df-mnf 9124  df-ltxr 9126  df-sub 9294  df-neg 9295
  Copyright terms: Public domain W3C validator