Definition df-neg 11501

Description: Define the negative of a number (unary minus). We use different symbols for unary minus (-) and subtraction (−) to prevent syntax ambiguity. See cneg 11499 for a discussion of this. (Contributed by NM, 10-Feb-1995.)

Assertion

Ref	Expression
df-neg	⊢ -𝐴 = (0 − 𝐴)

Detailed syntax breakdown of Definition df-neg

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	cneg 11499	. 2 class -𝐴
3		cc0 11157	. . 3 class 0
4		cmin 11498	. . 3 class −
5	3, 1, 4	co 7409	. 2 class (0 − 𝐴)
6	2, 5	wceq 1570	1 wff -𝐴 = (0 − 𝐴)

This definition is used by:  negeq  11506  nfnegd  11509  csbnegg  11511  negex  11512  negcl  11514  neg0  11561  negid  11562  negsub  11563  subneg  11564  negneg  11565  negsubdi  11571  renegcli  11576  addeq0  11694  mulneg1  11707  mulsubaddmulsub  11735  ltneg  11771  leneg  11774  ixi  11900  0mnnnnn0  12593  max0sub  13281  fz00m1  13633  fzshftral  13703  bernneq2  14327  discr1  14336  discr  14337  sgnneg  15206  cji  15279  rlimrege0  15699  rlimneg  15767  fallfacfwd  16155  binomfallfaclem2  16159  fsumcube  16179  divalglem1  16517  divalglem2  16518  m1bits  16563  bitsinv1lem  16564  prmdiv  16909  pcrec  16983  pcid  16998  4sqlem6  17068  4sqlem10  17072  chnub  18743  psgnunilem2  19656  cnheibor  25223  evth2  25228  dvlipcn  26261  dvfsumge  26289  ftc2  26311  vieta1lem2  26583  abelthlem8  26715  cospi  26750  coshalfpip  26772  ptolemy  26774  pige3ALT  26797  tanregt0  26816  argimgt0  26889  logcnlem3  26921  logf1o2  26927  advlogexp  26932  logtayl  26937  dvsqrt  27019  dvcnsqrt  27021  cxpcn3  27025  ang180lem3  27088  isosctrlem2  27096  asinlem  27145  atancj  27187  atanlogaddlem  27190  atantan  27200  dvatan  27212  emcllem7  27278  dmgmaddn0  27299  lgamgulmlem5  27309  lgambdd  27313  ftalem3  27351  1sgm2ppw  27476  dchrfi  27531  lgslem4  27576  lgseisen  27655  log2sumbnd  27820  colinearalglem4  29406  re0cj  33254  quad3d  33260  constrrtcc  34286  constrelextdg2  34298  2sqr3minply  34331  cos9thpiminplylem1  34333  qqhcn  34542  ballotlem1c  35060  quad3  36350  fz0n  36411  climlec3  36414  fwddifnp1  36846  qdiff  38162  tan2h  38449  broucube  38486  ftc2nc  38534  dvasin  38536  dvacos  38537  areacirclem1  38540  lcmineqlem7  42999  lcmineqlem10  43002  lcmineqlem12  43004  aks4d1p1p7  43038  posbezout  43064  bcle2d  43143  aks6d1c7lem1  43144  reelznn0nn  43447  mzpnegmpt  43687  binomcxplemrat  45272  binomcxplemnotnn0  45278  negcncfg  46807  itgsinexplem1  46880  stoweidlem34  46960  stirlinglem5  47004  fourierdlem36  47069  fourierdlem89  47121  fourierdlem90  47122  fourierdlem91  47123  fourierdlem107  47139  etransclem9  47169  etransclem14  47174  etransclem28  47188  etransclem35  47195  etransclem46  47206  resubcnnred  48290  m1modmmod  48350  gpgedgvtx0  49075  gpg3kgrtriex  49103  pgnbgreunbgrlem2lem1  49128  pgnbgreunbgrlem2lem2  49129  0nodd  49183  line2  49780  itschlc0xyqsol  49795