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

Definition df-neg 9040
Description: Define the negative of a number (unary minus). We use different symbols for unary minus ( -u) and subtraction ( -) to prevent syntax ambiguity. See cneg 9038 for a discussion of this. (Contributed by NM, 10-Feb-1995.)
Assertion
Ref Expression
df-neg  |-  -u A  =  ( 0  -  A )

Detailed syntax breakdown of Definition df-neg
StepHypRef Expression
1 cA . . 3  class  A
21cneg 9038 . 2  class  -u A
3 cc0 8737 . . 3  class  0
4 cmin 9037 . . 3  class  -
53, 1, 4co 5858 . 2  class  ( 0  -  A )
62, 5wceq 1623 1  wff  -u A  =  ( 0  -  A )
Colors of variables: wff set class
This definition is referenced by:  negeq  9044  nfnegd  9047  csbnegg  9049  negex  9050  negcl  9052  neg0  9093  negid  9094  negsub  9095  subneg  9096  negneg  9097  negsubdi  9103  renegcli  9108  mulneg1  9216  ltneg  9274  leneg  9277  ixi  9397  max0sub  10523  fzshftral  10869  bernneq2  11228  discr1  11237  discr  11238  cji  11644  rlimrege0  12053  rlimneg  12120  divalglem1  12593  divalglem2  12594  m1bits  12631  bitsinv1lem  12632  prmdiv  12853  pcrec  12911  pcid  12925  4sqlem6  12990  4sqlem10  12994  cnheibor  18453  evth2  18458  dvlipcn  19341  dvfsumge  19369  ftc2  19391  vieta1lem2  19691  abelthlem8  19815  cospi  19840  coshalfpip  19862  ptolemy  19864  pige3  19885  tanregt0  19901  argimgt0  19966  logcnlem3  19991  logf1o2  19997  advlogexp  20002  logtayl  20007  dvsqr  20084  cxpcn3  20088  ang180lem3  20109  isosctrlem2  20119  asinlem  20164  atancj  20206  atanlogaddlem  20209  atantan  20219  dvatan  20231  emcllem7  20295  ftalem3  20312  1sgm2ppw  20439  dchrfi  20494  lgslem4  20538  lgseisen  20592  log2sumbnd  20693  addinv  21019  addeq0  23043  ballotlem1c  23066  dmgmaddn0  23695  fz0n  24097  colinearalglem4  24537  fsumcube  24795  dvreasin  24923  dvreacos  24924  areacirclem2  24925  mzpnegmpt  26822  psgnunilem2  27418  itgsinexplem1  27748  stoweidlem34  27783  stirlinglem5  27827
  Copyright terms: Public domain W3C validator