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

Definition df-neg 8994
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 8992 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 8992 . 2  class  -u A
3 cc0 8691 . . 3  class  0
4 cmin 8991 . . 3  class  -
53, 1, 4co 5778 . 2  class  ( 0  -  A )
62, 5wceq 1619 1  wff  -u A  =  ( 0  -  A )
Colors of variables: wff set class
This definition is referenced by:  negeq  8998  nfnegd  9001  csbnegg  9003  negex  9004  negcl  9006  neg0  9047  negid  9048  negsub  9049  subneg  9050  negneg  9051  negsubdi  9057  renegcli  9062  mulneg1  9170  ltneg  9228  leneg  9231  ixi  9351  max0sub  10475  fzshftral  10821  bernneq2  11180  discr1  11189  discr  11190  cji  11595  rlimrege0  12004  rlimneg  12071  divalglem1  12541  divalglem2  12542  m1bits  12579  bitsinv1lem  12580  prmdiv  12801  pcrec  12859  pcid  12873  4sqlem6  12938  4sqlem10  12942  cnheibor  18401  evth2  18406  dvlipcn  19289  dvfsumge  19317  ftc2  19339  vieta1lem2  19639  abelthlem8  19763  cospi  19788  coshalfpip  19810  ptolemy  19812  pige3  19833  tanregt0  19849  argimgt0  19914  logcnlem3  19939  logf1o2  19945  advlogexp  19950  logtayl  19955  dvsqr  20032  cxpcn3  20036  ang180lem3  20057  isosctrlem2  20067  asinlem  20112  atancj  20154  atanlogaddlem  20157  atantan  20167  dvatan  20179  emcllem7  20243  ftalem3  20260  1sgm2ppw  20387  dchrfi  20442  lgslem4  20486  lgseisen  20540  log2sumbnd  20641  addinv  20965  addeq0  22990  ballotlem1c  23013  dmgmaddn0  23053  fz0n  23454  colinearalglem4  23898  fsumcube  24156  mzpnegmpt  26175  psgnunilem2  26771  stoweidlem34  27104
  Copyright terms: Public domain W3C validator