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 10865
Description: Define the negative of a number (unary minus). We use different symbols for unary minus (-) and subtraction () to prevent syntax ambiguity. See cneg 10863 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 10863 . 2 class -𝐴
3 cc0 10529 . . 3 class 0
4 cmin 10862 . . 3 class
53, 1, 4co 7151 . 2 class (0 − 𝐴)
62, 5wceq 1530 1 wff -𝐴 = (0 − 𝐴)
Colors of variables: wff setvar class
This definition is referenced by:  negeq  10870  nfnegd  10873  csbnegg  10875  negex  10876  negcl  10878  neg0  10924  negid  10925  negsub  10926  subneg  10927  negneg  10928  negsubdi  10934  renegcli  10939  addeq0  11055  mulneg1  11068  mulsubaddmulsub  11096  ltneg  11132  leneg  11135  ixi  11261  0mnnnnn0  11921  max0sub  12582  fzshftral  12988  bernneq2  13584  discr1  13593  discr  13594  cji  14511  rlimrege0  14929  rlimneg  14996  risefall0lem  15372  fallfacfwd  15382  binomfallfaclem2  15386  fsumcube  15406  divalglem1  15737  divalglem2  15738  m1bits  15781  bitsinv1lem  15782  prmdiv  16114  pcrec  16187  pcid  16201  4sqlem6  16271  4sqlem10  16275  psgnunilem2  18545  cnheibor  23474  evth2  23479  dvlipcn  24506  dvfsumge  24534  ftc2  24556  vieta1lem2  24815  abelthlem8  24942  cospi  24973  coshalfpip  24995  ptolemy  24997  pige3ALT  25020  tanregt0  25036  argimgt0  25108  logcnlem3  25140  logf1o2  25146  advlogexp  25151  logtayl  25156  dvsqrt  25236  dvcnsqrt  25238  cxpcn3  25242  ang180lem3  25302  isosctrlem2  25310  asinlem  25359  atancj  25401  atanlogaddlem  25404  atantan  25414  dvatan  25426  emcllem7  25493  dmgmaddn0  25514  lgamgulmlem5  25524  lgambdd  25528  ftalem3  25566  1sgm2ppw  25690  dchrfi  25745  lgslem4  25790  lgseisen  25869  log2sumbnd  26034  colinearalglem4  26610  qqhcn  31119  ballotlem1c  31652  sgnneg  31685  quad3  32798  fz0n  32847  climlec3  32850  fwddifnp1  33511  tan2h  34752  broucube  34794  ftc2nc  34844  dvasin  34846  dvacos  34847  areacirclem1  34850  mzpnegmpt  39203  binomcxplemrat  40544  binomcxplemnotnn0  40550  negcncfg  42026  itgsinexplem1  42101  stoweidlem34  42182  stirlinglem5  42226  fourierdlem36  42291  fourierdlem89  42343  fourierdlem90  42344  fourierdlem91  42345  fourierdlem107  42361  etransclem9  42391  etransclem14  42396  etransclem28  42410  etransclem35  42417  etransclem46  42428  resubcnnred  43367  0nodd  43906  m1modmmod  44410  line2  44568  itschlc0xyqsol  44583
  Copyright terms: Public domain W3C validator