Definition df-neg 9831

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 9829 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 9829	. 2
3		cc0 9513	. . 3
4		cmin 9828	. . 3
5	3, 1, 4	co 6296	. 2
6	2, 5	wceq 1395	1

This definition is referenced by:  negeq  9835  nfnegd  9838  csbnegg  9840  negex  9841  negcl  9843  neg0  9888  negid  9889  negsub  9890  subneg  9891  negneg  9892  negsubdi  9898  renegcli  9903  mulneg1  10018  ltneg  10077  leneg  10080  ixi  10203  0mnnnnn0  10853  max0sub  11424  fzshftral  11795  bernneq2  12293  discr1  12302  discr  12303  cji  12992  rlimrege0  13402  rlimneg  13469  divalglem1  14052  divalglem2  14053  m1bits  14090  bitsinv1lem  14091  prmdiv  14315  pcrec  14382  pcid  14396  4sqlem6  14461  4sqlem10  14465  psgnunilem2  16520  cnheibor  21455  evth2  21460  dvlipcn  22395  dvfsumge  22423  ftc2  22445  vieta1lem2  22707  abelthlem8  22834  cospi  22865  coshalfpip  22887  ptolemy  22889  pige3  22910  tanregt0  22926  argimgt0  22997  logcnlem3  23025  logf1o2  23031  advlogexp  23036  logtayl  23041  dvsqrt  23118  cxpcn3  23122  ang180lem3  23143  isosctrlem2  23153  asinlem  23199  atancj  23241  atanlogaddlem  23244  atantan  23254  dvatan  23266  emcllem7  23331  ftalem3  23348  1sgm2ppw  23475  dchrfi  23530  lgslem4  23574  lgseisen  23628  log2sumbnd  23729  colinearalglem4  24212  addinv  25354  addeq0  27558  qqhcn  27972  ballotlem1c  28446  sgnneg  28479  dmgmaddn0  28565  lgamgulmlem5  28575  lgambdd  28579  quad3  29024  fz0n  29110  climlec3  29120  risefall0lem  29148  fallfacfwd  29158  binomfallfaclem2  29162  fsumcube  29822  tan2h  30047  ftc2nc  30099  dvcnsqrt  30101  dvasin  30103  dvacos  30104  areacirclem1  30107  mzpnegmpt  30676  binomcxplemrat  31255  binomcxplemnotnn0  31261  negcncfg  31683  itgsinexplem1  31752  stoweidlem34  31816  stirlinglem5  31860  fourierdlem36  31925  fourierdlem89  31978  fourierdlem90  31979  fourierdlem91  31980  fourierdlem107  31996  etransclem9  32026  etransclem14  32031  etransclem28  32045  etransclem35  32052  etransclem46  32063  0nodd  32498