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

Definition df-neg 9056
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 9054 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 9054 . 2  class  -u A
3 cc0 8753 . . 3  class  0
4 cmin 9053 . . 3  class  -
53, 1, 4co 5874 . 2  class  ( 0  -  A )
62, 5wceq 1632 1  wff  -u A  =  ( 0  -  A )
Colors of variables: wff set class
This definition is referenced by:  negeq  9060  nfnegd  9063  csbnegg  9065  negex  9066  negcl  9068  neg0  9109  negid  9110  negsub  9111  subneg  9112  negneg  9113  negsubdi  9119  renegcli  9124  mulneg1  9232  ltneg  9290  leneg  9293  ixi  9413  max0sub  10539  fzshftral  10885  bernneq2  11244  discr1  11253  discr  11254  cji  11660  rlimrege0  12069  rlimneg  12136  divalglem1  12609  divalglem2  12610  m1bits  12647  bitsinv1lem  12648  prmdiv  12869  pcrec  12927  pcid  12941  4sqlem6  13006  4sqlem10  13010  cnheibor  18469  evth2  18474  dvlipcn  19357  dvfsumge  19385  ftc2  19407  vieta1lem2  19707  abelthlem8  19831  cospi  19856  coshalfpip  19878  ptolemy  19880  pige3  19901  tanregt0  19917  argimgt0  19982  logcnlem3  20007  logf1o2  20013  advlogexp  20018  logtayl  20023  dvsqr  20100  cxpcn3  20104  ang180lem3  20125  isosctrlem2  20135  asinlem  20180  atancj  20222  atanlogaddlem  20225  atantan  20235  dvatan  20247  emcllem7  20311  ftalem3  20328  1sgm2ppw  20455  dchrfi  20510  lgslem4  20554  lgseisen  20608  log2sumbnd  20709  addinv  21035  addeq0  23059  ballotlem1c  23082  dmgmaddn0  23710  fz0n  24112  colinearalglem4  24609  fsumcube  24867  dvreasin  25026  dvreacos  25027  areacirclem2  25028  mzpnegmpt  26925  psgnunilem2  27521  itgsinexplem1  27851  stoweidlem34  27886  stirlinglem5  27930
  Copyright terms: Public domain W3C validator