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

Definition df-neg 9286
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 9284 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 9284 . 2  class  -u A
3 cc0 8982 . . 3  class  0
4 cmin 9283 . . 3  class  -
53, 1, 4co 6073 . 2  class  ( 0  -  A )
62, 5wceq 1652 1  wff  -u A  =  ( 0  -  A )
Colors of variables: wff set class
This definition is referenced by:  negeq  9290  nfnegd  9293  csbnegg  9295  negex  9296  negcl  9298  neg0  9339  negid  9340  negsub  9341  subneg  9342  negneg  9343  negsubdi  9349  renegcli  9354  mulneg1  9462  ltneg  9520  leneg  9523  ixi  9643  max0sub  10774  fzshftral  11126  bernneq2  11498  discr1  11507  discr  11508  cji  11956  rlimrege0  12365  rlimneg  12432  divalglem1  12906  divalglem2  12907  m1bits  12944  bitsinv1lem  12945  prmdiv  13166  pcrec  13224  pcid  13238  4sqlem6  13303  4sqlem10  13307  cnheibor  18972  evth2  18977  dvlipcn  19870  dvfsumge  19898  ftc2  19920  vieta1lem2  20220  abelthlem8  20347  cospi  20372  coshalfpip  20394  ptolemy  20396  pige3  20417  tanregt0  20433  argimgt0  20499  logcnlem3  20527  logf1o2  20533  advlogexp  20538  logtayl  20543  dvsqr  20620  cxpcn3  20624  ang180lem3  20645  isosctrlem2  20655  asinlem  20700  atancj  20742  atanlogaddlem  20745  atantan  20755  dvatan  20767  emcllem7  20832  ftalem3  20849  1sgm2ppw  20976  dchrfi  21031  lgslem4  21075  lgseisen  21129  log2sumbnd  21230  addinv  21932  addeq0  24106  qqhcn  24367  ballotlem1c  24757  dmgmaddn0  24799  lgamgulmlem5  24809  lgambdd  24813  fz0n  25194  climlec3  25206  risefall0lem  25334  fallfacfwd  25344  binomfallfaclem2  25348  colinearalglem4  25840  fsumcube  26098  ftc2nc  26279  dvreasin  26280  dvreacos  26281  areacirclem2  26282  mzpnegmpt  26792  psgnunilem2  27386  itgsinexplem1  27715  stoweidlem34  27750  stirlinglem5  27794  0mnnnnn0  28080
  Copyright terms: Public domain W3C validator