Definition df-neg 10269

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 10267 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

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	cneg 10267	. 2 class -u A
3		cc0 9936	. . 3 class 0
4		cmin 10266	. . 3 class -
5	3, 1, 4	co 6650	. 2 class ( 0 - A )
6	2, 5	wceq 1483	1 wff -u A = ( 0 - A )

This definition is referenced by:  negeq  10273  nfnegd  10276  csbnegg  10278  negex  10279  negcl  10281  neg0  10327  negid  10328  negsub  10329  subneg  10330  negneg  10331  negsubdi  10337  renegcli  10342  mulneg1  10466  ltneg  10528  leneg  10531  ixi  10656  0mnnnnn0  11325  max0sub  12027  fzshftral  12428  bernneq2  12991  discr1  13000  discr  13001  cji  13899  rlimrege0  14310  rlimneg  14377  risefall0lem  14757  fallfacfwd  14767  binomfallfaclem2  14771  fsumcube  14791  divalglem1  15117  divalglem2  15118  m1bits  15162  bitsinv1lem  15163  prmdiv  15490  pcrec  15563  pcid  15577  4sqlem6  15647  4sqlem10  15651  psgnunilem2  17915  cnheibor  22754  evth2  22759  dvlipcn  23757  dvfsumge  23785  ftc2  23807  vieta1lem2  24066  abelthlem8  24193  cospi  24224  coshalfpip  24246  ptolemy  24248  pige3  24269  tanregt0  24285  argimgt0  24358  logcnlem3  24390  logf1o2  24396  advlogexp  24401  logtayl  24406  dvsqrt  24483  dvcnsqrt  24485  cxpcn3  24489  ang180lem3  24541  isosctrlem2  24549  asinlem  24595  atancj  24637  atanlogaddlem  24640  atantan  24650  dvatan  24662  emcllem7  24728  dmgmaddn0  24749  lgamgulmlem5  24759  lgambdd  24763  ftalem3  24801  1sgm2ppw  24925  dchrfi  24980  lgslem4  25025  lgseisen  25104  log2sumbnd  25233  colinearalglem4  25789  addeq0  29510  qqhcn  30035  ballotlem1c  30569  sgnneg  30602  quad3  31564  fz0n  31616  climlec3  31619  fwddifnp1  32272  tan2h  33401  broucube  33443  ftc2nc  33494  dvasin  33496  dvacos  33497  areacirclem1  33500  mzpnegmpt  37307  binomcxplemrat  38549  binomcxplemnotnn0  38555  negcncfg  40094  itgsinexplem1  40169  stoweidlem34  40251  stirlinglem5  40295  fourierdlem36  40360  fourierdlem89  40412  fourierdlem90  40413  fourierdlem91  40414  fourierdlem107  40430  etransclem9  40460  etransclem14  40465  etransclem28  40479  etransclem35  40486  etransclem46  40497  0nodd  41810  m1modmmod  42316