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

Definition df-neg 8973
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 8971 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 8971 . 2  class  -u A
3 cc0 8670 . . 3  class  0
4 cmin 8970 . . 3  class  -
53, 1, 4co 5757 . 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  8977  nfnegd  8980  csbnegg  8982  negex  8983  negcl  8985  neg0  9026  negid  9027  negsub  9028  subneg  9029  negneg  9030  negsubdi  9036  renegcli  9041  mulneg1  9149  ltneg  9207  leneg  9210  ixi  9330  max0sub  10454  fzshftral  10800  bernneq2  11159  discr1  11168  discr  11169  cji  11574  rlimrege0  11983  rlimneg  12050  divalglem1  12520  divalglem2  12521  m1bits  12558  bitsinv1lem  12559  prmdiv  12780  pcrec  12838  pcid  12852  4sqlem6  12917  4sqlem10  12921  cnheibor  18380  evth2  18385  dvlipcn  19268  dvfsumge  19296  ftc2  19318  vieta1lem2  19618  abelthlem8  19742  cospi  19767  coshalfpip  19789  ptolemy  19791  pige3  19812  tanregt0  19828  argimgt0  19893  logcnlem3  19918  logf1o2  19924  advlogexp  19929  logtayl  19934  dvsqr  20011  cxpcn3  20015  ang180lem3  20036  isosctrlem2  20046  asinlem  20091  atancj  20133  atanlogaddlem  20136  atantan  20146  dvatan  20158  emcllem7  20222  ftalem3  20239  1sgm2ppw  20366  dchrfi  20421  lgslem4  20465  lgseisen  20519  log2sumbnd  20620  addinv  20944  addeq0  22969  ballotlem1c  22992  dmgmaddn0  23032  fz0n  23433  colinearalglem4  23877  fsumcube  24135  mzpnegmpt  26154  psgnunilem2  26750  stoweidlem34  27083
  Copyright terms: Public domain W3C validator