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

Definition df-neg 9299
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 9297 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 9297 . 2  class  -u A
3 cc0 8995 . . 3  class  0
4 cmin 9296 . . 3  class  -
53, 1, 4co 6084 . 2  class  ( 0  -  A )
62, 5wceq 1653 1  wff  -u A  =  ( 0  -  A )
Colors of variables: wff set class
This definition is referenced by:  negeq  9303  nfnegd  9306  csbnegg  9308  negex  9309  negcl  9311  neg0  9352  negid  9353  negsub  9354  subneg  9355  negneg  9356  negsubdi  9362  renegcli  9367  mulneg1  9475  ltneg  9533  leneg  9536  ixi  9656  max0sub  10787  fzshftral  11139  bernneq2  11511  discr1  11520  discr  11521  cji  11969  rlimrege0  12378  rlimneg  12445  divalglem1  12919  divalglem2  12920  m1bits  12957  bitsinv1lem  12958  prmdiv  13179  pcrec  13237  pcid  13251  4sqlem6  13316  4sqlem10  13320  cnheibor  18985  evth2  18990  dvlipcn  19883  dvfsumge  19911  ftc2  19933  vieta1lem2  20233  abelthlem8  20360  cospi  20385  coshalfpip  20407  ptolemy  20409  pige3  20430  tanregt0  20446  argimgt0  20512  logcnlem3  20540  logf1o2  20546  advlogexp  20551  logtayl  20556  dvsqr  20633  cxpcn3  20637  ang180lem3  20658  isosctrlem2  20668  asinlem  20713  atancj  20755  atanlogaddlem  20758  atantan  20768  dvatan  20780  emcllem7  20845  ftalem3  20862  1sgm2ppw  20989  dchrfi  21044  lgslem4  21088  lgseisen  21142  log2sumbnd  21243  addinv  21945  addeq0  24119  qqhcn  24380  ballotlem1c  24770  dmgmaddn0  24812  lgamgulmlem5  24822  lgambdd  24826  fz0n  25207  climlec3  25219  risefall0lem  25347  fallfacfwd  25357  binomfallfaclem2  25361  colinearalglem4  25853  fsumcube  26111  tan2h  26252  ftc2nc  26303  dvreasin  26304  dvreacos  26305  areacirclem1  26306  mzpnegmpt  26815  psgnunilem2  27409  itgsinexplem1  27738  stoweidlem34  27773  stirlinglem5  27817  0mnnnnn0  28118
  Copyright terms: Public domain W3C validator