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

Definition df-neg 9037
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 9035 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 9035 . 2  class  -u A
3 cc0 8734 . . 3  class  0
4 cmin 9034 . . 3  class  -
53, 1, 4co 5821 . 2  class  ( 0  -  A )
62, 5wceq 1625 1  wff  -u A  =  ( 0  -  A )
Colors of variables: wff set class
This definition is referenced by:  negeq  9041  nfnegd  9044  csbnegg  9046  negex  9047  negcl  9049  neg0  9090  negid  9091  negsub  9092  subneg  9093  negneg  9094  negsubdi  9100  renegcli  9105  mulneg1  9213  ltneg  9271  leneg  9274  ixi  9394  max0sub  10519  fzshftral  10865  bernneq2  11224  discr1  11233  discr  11234  cji  11640  rlimrege0  12049  rlimneg  12116  divalglem1  12589  divalglem2  12590  m1bits  12627  bitsinv1lem  12628  prmdiv  12849  pcrec  12907  pcid  12921  4sqlem6  12986  4sqlem10  12990  cnheibor  18449  evth2  18454  dvlipcn  19337  dvfsumge  19365  ftc2  19387  vieta1lem2  19687  abelthlem8  19811  cospi  19836  coshalfpip  19858  ptolemy  19860  pige3  19881  tanregt0  19897  argimgt0  19962  logcnlem3  19987  logf1o2  19993  advlogexp  19998  logtayl  20003  dvsqr  20080  cxpcn3  20084  ang180lem3  20105  isosctrlem2  20115  asinlem  20160  atancj  20202  atanlogaddlem  20205  atantan  20215  dvatan  20227  emcllem7  20291  ftalem3  20308  1sgm2ppw  20435  dchrfi  20490  lgslem4  20534  lgseisen  20588  log2sumbnd  20689  addinv  21013  addeq0  23038  ballotlem1c  23061  dmgmaddn0  23101  fz0n  23502  colinearalglem4  23946  fsumcube  24204  mzpnegmpt  26223  psgnunilem2  26819  itgsinexplem1  27149  stoweidlem34  27184  stirlinglem5  27228
  Copyright terms: Public domain W3C validator