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

Definition df-neg 9250
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 9248 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 9248 . 2  class  -u A
3 cc0 8946 . . 3  class  0
4 cmin 9247 . . 3  class  -
53, 1, 4co 6040 . 2  class  ( 0  -  A )
62, 5wceq 1649 1  wff  -u A  =  ( 0  -  A )
Colors of variables: wff set class
This definition is referenced by:  negeq  9254  nfnegd  9257  csbnegg  9259  negex  9260  negcl  9262  neg0  9303  negid  9304  negsub  9305  subneg  9306  negneg  9307  negsubdi  9313  renegcli  9318  mulneg1  9426  ltneg  9484  leneg  9487  ixi  9607  max0sub  10738  fzshftral  11089  bernneq2  11461  discr1  11470  discr  11471  cji  11919  rlimrege0  12328  rlimneg  12395  divalglem1  12869  divalglem2  12870  m1bits  12907  bitsinv1lem  12908  prmdiv  13129  pcrec  13187  pcid  13201  4sqlem6  13266  4sqlem10  13270  cnheibor  18933  evth2  18938  dvlipcn  19831  dvfsumge  19859  ftc2  19881  vieta1lem2  20181  abelthlem8  20308  cospi  20333  coshalfpip  20355  ptolemy  20357  pige3  20378  tanregt0  20394  argimgt0  20460  logcnlem3  20488  logf1o2  20494  advlogexp  20499  logtayl  20504  dvsqr  20581  cxpcn3  20585  ang180lem3  20606  isosctrlem2  20616  asinlem  20661  atancj  20703  atanlogaddlem  20706  atantan  20716  dvatan  20728  emcllem7  20793  ftalem3  20810  1sgm2ppw  20937  dchrfi  20992  lgslem4  21036  lgseisen  21090  log2sumbnd  21191  addinv  21893  addeq0  24067  qqhcn  24328  ballotlem1c  24718  dmgmaddn0  24760  lgamgulmlem5  24770  lgambdd  24774  fz0n  25155  climlec3  25167  risefall0lem  25294  fallfacfwd  25303  binomfallfaclem2  25307  colinearalglem4  25752  fsumcube  26010  dvreasin  26179  dvreacos  26180  areacirclem2  26181  mzpnegmpt  26691  psgnunilem2  27286  itgsinexplem1  27615  stoweidlem34  27650  stirlinglem5  27694  0mnnnnn0  27971
  Copyright terms: Public domain W3C validator