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 10254
Description: Define the negative of a number (unary minus). We use different symbols for unary minus (-) and subtraction () to prevent syntax ambiguity. See cneg 10252 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 10252 . 2 class -𝐴
3 cc0 9921 . . 3 class 0
4 cmin 10251 . . 3 class
53, 1, 4co 6635 . 2 class (0 − 𝐴)
62, 5wceq 1481 1 wff -𝐴 = (0 − 𝐴)
Colors of variables: wff setvar class
This definition is referenced by:  negeq  10258  nfnegd  10261  csbnegg  10263  negex  10264  negcl  10266  neg0  10312  negid  10313  negsub  10314  subneg  10315  negneg  10316  negsubdi  10322  renegcli  10327  mulneg1  10451  ltneg  10513  leneg  10516  ixi  10641  0mnnnnn0  11310  max0sub  12012  fzshftral  12412  bernneq2  12974  discr1  12983  discr  12984  cji  13880  rlimrege0  14291  rlimneg  14358  risefall0lem  14738  fallfacfwd  14748  binomfallfaclem2  14752  fsumcube  14772  divalglem1  15098  divalglem2  15099  m1bits  15143  bitsinv1lem  15144  prmdiv  15471  pcrec  15544  pcid  15558  4sqlem6  15628  4sqlem10  15632  psgnunilem2  17896  cnheibor  22735  evth2  22740  dvlipcn  23738  dvfsumge  23766  ftc2  23788  vieta1lem2  24047  abelthlem8  24174  cospi  24205  coshalfpip  24227  ptolemy  24229  pige3  24250  tanregt0  24266  argimgt0  24339  logcnlem3  24371  logf1o2  24377  advlogexp  24382  logtayl  24387  dvsqrt  24464  dvcnsqrt  24466  cxpcn3  24470  ang180lem3  24522  isosctrlem2  24530  asinlem  24576  atancj  24618  atanlogaddlem  24621  atantan  24631  dvatan  24643  emcllem7  24709  dmgmaddn0  24730  lgamgulmlem5  24740  lgambdd  24744  ftalem3  24782  1sgm2ppw  24906  dchrfi  24961  lgslem4  25006  lgseisen  25085  log2sumbnd  25214  colinearalglem4  25770  addeq0  29484  qqhcn  30009  ballotlem1c  30543  sgnneg  30576  quad3  31538  fz0n  31591  climlec3  31594  fwddifnp1  32247  tan2h  33372  broucube  33414  ftc2nc  33465  dvasin  33467  dvacos  33468  areacirclem1  33471  mzpnegmpt  37126  binomcxplemrat  38369  binomcxplemnotnn0  38375  negcncfg  39857  itgsinexplem1  39932  stoweidlem34  40014  stirlinglem5  40058  fourierdlem36  40123  fourierdlem89  40175  fourierdlem90  40176  fourierdlem91  40177  fourierdlem107  40193  etransclem9  40223  etransclem14  40228  etransclem28  40242  etransclem35  40249  etransclem46  40260  0nodd  41575  m1modmmod  42081
  Copyright terms: Public domain W3C validator