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 10432
Description: Define the negative of a number (unary minus). We use different symbols for unary minus (-) and subtraction () to prevent syntax ambiguity. See cneg 10430 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 10430 . 2 class -𝐴
3 cc0 10099 . . 3 class 0
4 cmin 10429 . . 3 class
53, 1, 4co 6801 . 2 class (0 − 𝐴)
62, 5wceq 1620 1 wff -𝐴 = (0 − 𝐴)
Colors of variables: wff setvar class
This definition is referenced by:  negeq  10436  nfnegd  10439  csbnegg  10441  negex  10442  negcl  10444  neg0  10490  negid  10491  negsub  10492  subneg  10493  negneg  10494  negsubdi  10500  renegcli  10505  mulneg1  10629  ltneg  10691  leneg  10694  ixi  10819  0mnnnnn0  11488  max0sub  12191  fzshftral  12592  bernneq2  13156  discr1  13165  discr  13166  cji  14069  rlimrege0  14480  rlimneg  14547  risefall0lem  14927  fallfacfwd  14937  binomfallfaclem2  14941  fsumcube  14961  divalglem1  15290  divalglem2  15291  m1bits  15335  bitsinv1lem  15336  prmdiv  15663  pcrec  15736  pcid  15750  4sqlem6  15820  4sqlem10  15824  psgnunilem2  18086  cnheibor  22926  evth2  22931  dvlipcn  23927  dvfsumge  23955  ftc2  23977  vieta1lem2  24236  abelthlem8  24363  cospi  24394  coshalfpip  24416  ptolemy  24418  pige3  24439  tanregt0  24455  argimgt0  24528  logcnlem3  24560  logf1o2  24566  advlogexp  24571  logtayl  24576  dvsqrt  24653  dvcnsqrt  24655  cxpcn3  24659  ang180lem3  24711  isosctrlem2  24719  asinlem  24765  atancj  24807  atanlogaddlem  24810  atantan  24820  dvatan  24832  emcllem7  24898  dmgmaddn0  24919  lgamgulmlem5  24929  lgambdd  24933  ftalem3  24971  1sgm2ppw  25095  dchrfi  25150  lgslem4  25195  lgseisen  25274  log2sumbnd  25403  colinearalglem4  25959  addeq0  29790  qqhcn  30315  ballotlem1c  30849  sgnneg  30882  quad3  31842  fz0n  31894  climlec3  31897  fwddifnp1  32549  tan2h  33683  broucube  33725  ftc2nc  33776  dvasin  33778  dvacos  33779  areacirclem1  33782  mzpnegmpt  37778  binomcxplemrat  39020  binomcxplemnotnn0  39026  negcncfg  40566  itgsinexplem1  40641  stoweidlem34  40723  stirlinglem5  40767  fourierdlem36  40832  fourierdlem89  40884  fourierdlem90  40885  fourierdlem91  40886  fourierdlem107  40902  etransclem9  40932  etransclem14  40937  etransclem28  40951  etransclem35  40958  etransclem46  40969  0nodd  42289  m1modmmod  42795
  Copyright terms: Public domain W3C validator