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 10024
Description: Define the negative of a number (unary minus). We use different symbols for unary minus (-) and subtraction () to prevent syntax ambiguity. See cneg 10022 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 10022 . 2 class -𝐴
3 cc0 9695 . . 3 class 0
4 cmin 10021 . . 3 class
53, 1, 4co 6431 . 2 class (0 − 𝐴)
62, 5wceq 1474 1 wff -𝐴 = (0 − 𝐴)
Colors of variables: wff setvar class
This definition is referenced by:  negeq  10028  nfnegd  10031  csbnegg  10033  negex  10034  negcl  10036  neg0  10082  negid  10083  negsub  10084  subneg  10085  negneg  10086  negsubdi  10092  renegcli  10097  mulneg1  10221  ltneg  10281  leneg  10284  ixi  10409  0mnnnnn0  11084  max0sub  11774  fzshftral  12169  bernneq2  12725  discr1  12734  discr  12735  cji  13610  rlimrege0  14028  rlimneg  14095  risefall0lem  14469  fallfacfwd  14479  binomfallfaclem2  14483  fsumcube  14503  divalglem1  14828  divalglem2  14829  divalglem2OLD  14830  m1bits  14877  bitsinv1lem  14878  prmdiv  15210  pcrec  15289  pcid  15303  4sqlem6  15373  4sqlem10  15377  psgnunilem2  17634  cnheibor  22489  evth2  22494  dvlipcn  23440  dvfsumge  23468  ftc2  23490  vieta1lem2  23758  abelthlem8  23888  cospi  23919  coshalfpip  23941  ptolemy  23943  pige3  23964  tanregt0  23980  argimgt0  24053  logcnlem3  24081  logf1o2  24087  advlogexp  24092  logtayl  24097  dvsqrt  24174  dvcnsqrt  24176  cxpcn3  24180  ang180lem3  24232  isosctrlem2  24240  asinlem  24286  atancj  24328  atanlogaddlem  24331  atantan  24341  dvatan  24353  emcllem7  24419  dmgmaddn0  24440  lgamgulmlem5  24450  lgambdd  24454  ftalem3  24492  1sgm2ppw  24618  dchrfi  24673  lgslem4  24718  lgseisen  24797  log2sumbnd  24926  colinearalglem4  25483  addeq0  28690  qqhcn  29163  ballotlem1c  29707  ballotlem1cOLD  29745  sgnneg  29778  quad3  30665  fz0n  30715  climlec3  30718  fwddifnp1  31281  tan2h  32465  broucube  32507  ftc2nc  32558  dvasin  32560  dvacos  32561  areacirclem1  32564  mzpnegmpt  36219  binomcxplemrat  37472  binomcxplemnotnn0  37478  negcncfg  38670  itgsinexplem1  38752  stoweidlem34  38834  stirlinglem5  38878  fourierdlem36  38944  fourierdlem89  38997  fourierdlem90  38998  fourierdlem91  38999  fourierdlem107  39015  etransclem9  39046  etransclem14  39051  etransclem28  39065  etransclem35  39072  etransclem46  39083  0nodd  41709  m1modmmod  42219
  Copyright terms: Public domain W3C validator