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

Definition df-neg 9950
Description: Define the negative of a number (unary minus). We use different symbols for unary minus (-) and subtraction () to prevent syntax ambiguity. See cneg 9948 for a discussion of this. (Contributed by NM, 10-Feb-1995.)
Assertion
Ref Expression
df-neg -𝐴 = (0 − 𝐴)

Detailed syntax breakdown of Definition df-neg
StepHypRef Expression
1 cA . . 3 class 𝐴
21cneg 9948 . 2 class -𝐴
3 cc0 9624 . . 3 class 0
4 cmin 9947 . . 3 class
53, 1, 4co 6363 . 2 class (0 − 𝐴)
62, 5wceq 1468 1 wff -𝐴 = (0 − 𝐴)
Colors of variables: wff setvar class
This definition is referenced by:  negeq  9954  nfnegd  9957  csbnegg  9959  negex  9960  negcl  9962  neg0  10007  negid  10008  negsub  10009  subneg  10010  negneg  10011  negsubdi  10017  renegcli  10022  mulneg1  10143  ltneg  10202  leneg  10205  ixi  10330  0mnnnnn0  10993  max0sub  11582  fzshftral  11980  bernneq2  12513  discr1  12522  discr  12523  cji  13382  rlimrege0  13803  rlimneg  13870  risefall0lem  14239  fallfacfwd  14249  binomfallfaclem2  14253  fsumcube  14273  divalglem1  14534  divalglem2  14535  divalglem2OLD  14536  m1bits  14576  bitsinv1lem  14577  prmdiv  14895  pcrec  14970  pcid  14984  4sqlem6  15049  4sqlem10  15053  psgnunilem2  17297  cnheibor  22141  evth2  22146  dvlipcn  23107  dvfsumge  23135  ftc2  23157  vieta1lem2  23425  abelthlem8  23555  cospi  23588  coshalfpip  23610  ptolemy  23612  pige3  23633  tanregt0  23649  argimgt0  23722  logcnlem3  23750  logf1o2  23756  advlogexp  23761  logtayl  23766  dvsqrt  23843  dvcnsqrt  23845  cxpcn3  23849  ang180lem3  23901  isosctrlem2  23909  asinlem  23955  atancj  23997  atanlogaddlem  24000  atantan  24010  dvatan  24022  emcllem7  24088  dmgmaddn0  24109  lgamgulmlem5  24119  lgambdd  24123  ftalem3  24160  1sgm2ppw  24289  dchrfi  24344  lgslem4  24388  lgseisen  24442  log2sumbnd  24543  colinearalglem4  25100  addinv  26243  addeq0  28476  qqhcn  28950  ballotlem1c  29494  ballotlem1cOLD  29532  sgnneg  29565  quad3  30454  fz0n  30516  climlec3  30520  fwddifnp1  31083  tan2h  32170  broucube  32212  ftc2nc  32264  dvasin  32266  dvacos  32267  areacirclem1  32270  mzpnegmpt  35826  binomcxplemrat  37056  binomcxplemnotnn0  37062  negcncfg  38167  itgsinexplem1  38249  stoweidlem34  38331  stirlinglem5  38376  fourierdlem36  38442  fourierdlem89  38495  fourierdlem90  38496  fourierdlem91  38497  fourierdlem107  38513  etransclem9  38544  etransclem14  38549  etransclem28  38563  etransclem35  38570  etransclem46  38581  0nodd  41000  m1modmmod  41513
  Copyright terms: Public domain W3C validator