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 10213
Description: Define the negative of a number (unary minus). We use different symbols for unary minus (-) and subtraction () to prevent syntax ambiguity. See cneg 10211 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 10211 . 2 class -𝐴
3 cc0 9880 . . 3 class 0
4 cmin 10210 . . 3 class
53, 1, 4co 6604 . 2 class (0 − 𝐴)
62, 5wceq 1480 1 wff -𝐴 = (0 − 𝐴)
Colors of variables: wff setvar class
This definition is referenced by:  negeq  10217  nfnegd  10220  csbnegg  10222  negex  10223  negcl  10225  neg0  10271  negid  10272  negsub  10273  subneg  10274  negneg  10275  negsubdi  10281  renegcli  10286  mulneg1  10410  ltneg  10472  leneg  10475  ixi  10600  0mnnnnn0  11269  max0sub  11970  fzshftral  12369  bernneq2  12931  discr1  12940  discr  12941  cji  13833  rlimrege0  14244  rlimneg  14311  risefall0lem  14682  fallfacfwd  14692  binomfallfaclem2  14696  fsumcube  14716  divalglem1  15041  divalglem2  15042  m1bits  15086  bitsinv1lem  15087  prmdiv  15414  pcrec  15487  pcid  15501  4sqlem6  15571  4sqlem10  15575  psgnunilem2  17836  cnheibor  22662  evth2  22667  dvlipcn  23661  dvfsumge  23689  ftc2  23711  vieta1lem2  23970  abelthlem8  24097  cospi  24128  coshalfpip  24150  ptolemy  24152  pige3  24173  tanregt0  24189  argimgt0  24262  logcnlem3  24290  logf1o2  24296  advlogexp  24301  logtayl  24306  dvsqrt  24383  dvcnsqrt  24385  cxpcn3  24389  ang180lem3  24441  isosctrlem2  24449  asinlem  24495  atancj  24537  atanlogaddlem  24540  atantan  24550  dvatan  24562  emcllem7  24628  dmgmaddn0  24649  lgamgulmlem5  24659  lgambdd  24663  ftalem3  24701  1sgm2ppw  24825  dchrfi  24880  lgslem4  24925  lgseisen  25004  log2sumbnd  25133  colinearalglem4  25689  addeq0  29350  qqhcn  29814  ballotlem1c  30347  sgnneg  30380  quad3  31269  fz0n  31321  climlec3  31324  fwddifnp1  31911  tan2h  33030  broucube  33072  ftc2nc  33123  dvasin  33125  dvacos  33126  areacirclem1  33129  mzpnegmpt  36784  binomcxplemrat  38028  binomcxplemnotnn0  38034  negcncfg  39394  itgsinexplem1  39473  stoweidlem34  39555  stirlinglem5  39599  fourierdlem36  39664  fourierdlem89  39716  fourierdlem90  39717  fourierdlem91  39718  fourierdlem107  39734  etransclem9  39764  etransclem14  39769  etransclem28  39783  etransclem35  39790  etransclem46  39801  0nodd  41095  m1modmmod  41601
  Copyright terms: Public domain W3C validator