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 10120
Description: Define the negative of a number (unary minus). We use different symbols for unary minus (-) and subtraction () to prevent syntax ambiguity. See cneg 10118 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 10118 . 2 class -𝐴
3 cc0 9792 . . 3 class 0
4 cmin 10117 . . 3 class
53, 1, 4co 6527 . 2 class (0 − 𝐴)
62, 5wceq 1474 1 wff -𝐴 = (0 − 𝐴)
Colors of variables: wff setvar class
This definition is referenced by:  negeq  10124  nfnegd  10127  csbnegg  10129  negex  10130  negcl  10132  neg0  10178  negid  10179  negsub  10180  subneg  10181  negneg  10182  negsubdi  10188  renegcli  10193  mulneg1  10317  ltneg  10377  leneg  10380  ixi  10505  0mnnnnn0  11172  max0sub  11860  fzshftral  12252  bernneq2  12808  discr1  12817  discr  12818  cji  13693  rlimrege0  14104  rlimneg  14171  risefall0lem  14542  fallfacfwd  14552  binomfallfaclem2  14556  fsumcube  14576  divalglem1  14901  divalglem2  14902  m1bits  14946  bitsinv1lem  14947  prmdiv  15274  pcrec  15347  pcid  15361  4sqlem6  15431  4sqlem10  15435  psgnunilem2  17684  cnheibor  22493  evth2  22498  dvlipcn  23478  dvfsumge  23506  ftc2  23528  vieta1lem2  23787  abelthlem8  23914  cospi  23945  coshalfpip  23967  ptolemy  23969  pige3  23990  tanregt0  24006  argimgt0  24079  logcnlem3  24107  logf1o2  24113  advlogexp  24118  logtayl  24123  dvsqrt  24200  dvcnsqrt  24202  cxpcn3  24206  ang180lem3  24258  isosctrlem2  24266  asinlem  24312  atancj  24354  atanlogaddlem  24357  atantan  24367  dvatan  24379  emcllem7  24445  dmgmaddn0  24466  lgamgulmlem5  24476  lgambdd  24480  ftalem3  24518  1sgm2ppw  24642  dchrfi  24697  lgslem4  24742  lgseisen  24821  log2sumbnd  24950  colinearalglem4  25507  addeq0  28704  qqhcn  29169  ballotlem1c  29702  sgnneg  29735  quad3  30624  fz0n  30675  climlec3  30678  fwddifnp1  31248  tan2h  32367  broucube  32409  ftc2nc  32460  dvasin  32462  dvacos  32463  areacirclem1  32466  mzpnegmpt  36121  binomcxplemrat  37367  binomcxplemnotnn0  37373  negcncfg  38563  itgsinexplem1  38642  stoweidlem34  38724  stirlinglem5  38768  fourierdlem36  38833  fourierdlem89  38885  fourierdlem90  38886  fourierdlem91  38887  fourierdlem107  38903  etransclem9  38933  etransclem14  38938  etransclem28  38952  etransclem35  38959  etransclem46  38970  0nodd  41595  m1modmmod  42105
  Copyright terms: Public domain W3C validator