MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-neg Unicode version

Definition df-neg 8920
Description: Define the negative of a number (unary minus). We use different symbols for unary minus ( -u) and subtraction ( -) to prevent syntax ambiguity. See cneg 8918 for a discussion of this. (Contributed by NM, 10-Feb-1995.)
Assertion
Ref Expression
df-neg  |-  -u A  =  ( 0  -  A )

Detailed syntax breakdown of Definition df-neg
StepHypRef Expression
1 cA . . 3  class  A
21cneg 8918 . 2  class  -u A
3 cc0 8617 . . 3  class  0
4 cmin 8917 . . 3  class  -
53, 1, 4co 5710 . 2  class  ( 0  -  A )
62, 5wceq 1619 1  wff  -u A  =  ( 0  -  A )
Colors of variables: wff set class
This definition is referenced by:  negeq  8924  nfnegd  8927  csbnegg  8929  negex  8930  negcl  8932  neg0  8973  negid  8974  negsub  8975  subneg  8976  negneg  8977  negsubdi  8983  renegcli  8988  mulneg1  9096  ltneg  9154  leneg  9157  ixi  9277  max0sub  10401  fzshftral  10747  bernneq2  11106  discr1  11115  discr  11116  cji  11521  rlimrege0  11930  rlimneg  11997  divalglem1  12467  divalglem2  12468  m1bits  12505  bitsinv1lem  12506  prmdiv  12727  pcrec  12785  pcid  12799  4sqlem6  12864  4sqlem10  12868  cnheibor  18285  evth2  18290  dvlipcn  19173  dvfsumge  19201  ftc2  19223  vieta1lem2  19523  abelthlem8  19647  cospi  19672  coshalfpip  19694  ptolemy  19696  pige3  19717  tanregt0  19733  argimgt0  19798  logcnlem3  19823  logf1o2  19829  advlogexp  19834  logtayl  19839  ang180lem3  19853  isosctrlem2  19863  dvsqr  19952  cxpcn3  19956  asinlem  19996  atancj  20038  atanlogaddlem  20041  atantan  20051  dvatan  20063  emcllem7  20127  ftalem3  20144  1sgm2ppw  20271  dchrfi  20326  lgslem4  20370  lgseisen  20424  log2sumbnd  20525  addinv  20849  dmgmaddn0  22866  fz0n  23267  colinearalglem4  23711  fsumcube  23969  mzpnegmpt  25988  psgnunilem2  26584
  Copyright terms: Public domain W3C validator