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 10862
Description: Define the negative of a number (unary minus). We use different symbols for unary minus (-) and subtraction () to prevent syntax ambiguity. See cneg 10860 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 10860 . 2 class -𝐴
3 cc0 10526 . . 3 class 0
4 cmin 10859 . . 3 class
53, 1, 4co 7145 . 2 class (0 − 𝐴)
62, 5wceq 1528 1 wff -𝐴 = (0 − 𝐴)
Colors of variables: wff setvar class
This definition is referenced by:  negeq  10867  nfnegd  10870  csbnegg  10872  negex  10873  negcl  10875  neg0  10921  negid  10922  negsub  10923  subneg  10924  negneg  10925  negsubdi  10931  renegcli  10936  addeq0  11052  mulneg1  11065  mulsubaddmulsub  11093  ltneg  11129  leneg  11132  ixi  11258  0mnnnnn0  11918  max0sub  12579  fzshftral  12985  bernneq2  13581  discr1  13590  discr  13591  cji  14508  rlimrege0  14926  rlimneg  14993  risefall0lem  15370  fallfacfwd  15380  binomfallfaclem2  15384  fsumcube  15404  divalglem1  15735  divalglem2  15736  m1bits  15779  bitsinv1lem  15780  prmdiv  16112  pcrec  16185  pcid  16199  4sqlem6  16269  4sqlem10  16273  psgnunilem2  18554  cnheibor  23488  evth2  23493  dvlipcn  24520  dvfsumge  24548  ftc2  24570  vieta1lem2  24829  abelthlem8  24956  cospi  24987  coshalfpip  25009  ptolemy  25011  pige3ALT  25034  tanregt0  25050  argimgt0  25122  logcnlem3  25154  logf1o2  25160  advlogexp  25165  logtayl  25170  dvsqrt  25250  dvcnsqrt  25252  cxpcn3  25256  ang180lem3  25316  isosctrlem2  25324  asinlem  25373  atancj  25415  atanlogaddlem  25418  atantan  25428  dvatan  25440  emcllem7  25507  dmgmaddn0  25528  lgamgulmlem5  25538  lgambdd  25542  ftalem3  25580  1sgm2ppw  25704  dchrfi  25759  lgslem4  25804  lgseisen  25883  log2sumbnd  26048  colinearalglem4  26623  qqhcn  31132  ballotlem1c  31665  sgnneg  31698  quad3  32811  fz0n  32860  climlec3  32863  fwddifnp1  33524  tan2h  34766  broucube  34808  ftc2nc  34858  dvasin  34860  dvacos  34861  areacirclem1  34864  mzpnegmpt  39221  binomcxplemrat  40562  binomcxplemnotnn0  40568  negcncfg  42044  itgsinexplem1  42119  stoweidlem34  42200  stirlinglem5  42244  fourierdlem36  42309  fourierdlem89  42361  fourierdlem90  42362  fourierdlem91  42363  fourierdlem107  42379  etransclem9  42409  etransclem14  42414  etransclem28  42428  etransclem35  42435  etransclem46  42446  resubcnnred  43385  0nodd  43924  m1modmmod  44479  line2  44637  itschlc0xyqsol  44652
  Copyright terms: Public domain W3C validator