Definition df-neg 9544

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 9542 for a discussion of this. (Contributed by NM, 10-Feb-1995.)

Assertion

Ref	Expression
df-neg

Detailed syntax breakdown of Definition df-neg

Step	Hyp	Ref	Expression
1		cA	. . 3
2	1	cneg 9542	. 2
3		cc0 9228	. . 3
4		cmin 9541	. . 3
5	3, 1, 4	co 6061	. 2
6	2, 5	wceq 1687	1

This definition is referenced by:  negeq  9548  nfnegd  9551  csbnegg  9553  negex  9554  negcl  9556  neg0  9601  negid  9602  negsub  9603  subneg  9604  negneg  9605  negsubdi  9611  renegcli  9616  mulneg1  9727  ltneg  9785  leneg  9788  ixi  9911  0mnnnnn0  10558  max0sub  11111  fzshftral  11488  bernneq2  11932  discr1  11941  discr  11942  cji  12589  rlimrege0  12998  rlimneg  13065  divalglem1  13538  divalglem2  13539  m1bits  13576  bitsinv1lem  13577  prmdiv  13800  pcrec  13865  pcid  13879  4sqlem6  13944  4sqlem10  13948  psgnunilem2  15938  cnheibor  20227  evth2  20232  dvlipcn  21166  dvfsumge  21194  ftc2  21216  vieta1lem2  21518  abelthlem8  21645  cospi  21675  coshalfpip  21697  ptolemy  21699  pige3  21720  tanregt0  21736  argimgt0  21802  logcnlem3  21830  logf1o2  21836  advlogexp  21841  logtayl  21846  dvsqr  21923  cxpcn3  21927  ang180lem3  21948  isosctrlem2  21958  asinlem  22004  atancj  22046  atanlogaddlem  22049  atantan  22059  dvatan  22071  emcllem7  22136  ftalem3  22153  1sgm2ppw  22280  dchrfi  22335  lgslem4  22379  lgseisen  22433  log2sumbnd  22534  colinearalglem4  22834  addinv  23518  addeq0  25715  qqhcn  26129  ballotlem1c  26593  sgnneg  26626  dmgmaddn0  26712  lgamgulmlem5  26722  lgambdd  26726  fz0n  27091  climlec3  27103  risefall0lem  27231  fallfacfwd  27241  binomfallfaclem2  27245  fsumcube  27905  tan2h  28095  ftc2nc  28147  dvcnsqr  28149  dvasin  28151  dvacos  28152  areacirclem1  28155  mzpnegmpt  28753  itgsinexplem1  29468  stoweidlem34  29503  stirlinglem5  29547