Definition df-neg 11568

Description: Define the negative of a number (unary minus). We use different symbols for unary minus (-) and subtraction (−) to prevent syntax ambiguity. See cneg 11566 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 11566	. 2 class -𝐴
3		cc0 11224	. . 3 class 0
4		cmin 11565	. . 3 class −
5	3, 1, 4	co 7440	. 2 class (0 − 𝐴)
6	2, 5	wceq 1570	1 wff -𝐴 = (0 − 𝐴)

This definition is used by:  negeq  11573  nfnegd  11576  csbnegg  11578  negex  11579  negcl  11581  neg0  11628  negid  11629  negsub  11630  subneg  11631  negneg  11632  negsubdi  11638  renegcli  11643  addeq0  11763  mulneg1  11776  mulsubaddmulsub  11804  ltneg  11840  leneg  11843  ixi  11969  0mnnnnn0  12662  max0sub  13350  fz00m1  13703  fzshftral  13773  bernneq2  14398  discr1  14407  discr  14408  sgnneg  15279  cji  15352  rlimrege0  15772  rlimneg  15840  fallfacfwd  16228  binomfallfaclem2  16232  fsumcube  16252  divalglem1  16590  divalglem2  16591  m1bits  16636  bitsinv1lem  16637  prmdiv  16988  pcrec  17062  pcid  17077  4sqlem6  17147  4sqlem10  17151  chnub  18822  psgnunilem2  19736  cnheibor  25303  evth2  25308  dvlipcn  26341  dvfsumge  26369  ftc2  26391  vieta1lem2  26661  abelthlem8  26793  cospi  26828  coshalfpip  26850  ptolemy  26852  pige3ALT  26875  tanregt0  26894  argimgt0  26967  logcnlem3  26999  logf1o2  27005  advlogexp  27010  logtayl  27015  dvsqrt  27097  dvcnsqrt  27099  cxpcn3  27103  ang180lem3  27166  isosctrlem2  27174  asinlem  27223  atancj  27265  atanlogaddlem  27268  atantan  27278  dvatan  27290  emcllem7  27356  dmgmaddn0  27377  lgamgulmlem5  27387  lgambdd  27391  ftalem3  27429  1sgm2ppw  27554  dchrfi  27609  lgslem4  27654  lgseisen  27733  log2sumbnd  27898  colinearalglem4  29514  re0cj  33402  quad3d  33408  constrrtcc  34434  constrelextdg2  34446  2sqr3minply  34479  cos9thpiminplylem1  34481  qqhcn  34690  ballotlem1c  35207  quad3  36601  fz0n  36673  climlec3  36676  fwddifnp1  37107  qdiff  38439  tan2h  38726  broucube  38763  ftc2nc  38811  dvasin  38813  dvacos  38814  areacirclem1  38817  lcmineqlem7  43276  lcmineqlem10  43279  lcmineqlem12  43281  aks4d1p1p7  43315  posbezout  43341  bcle2d  43420  aks6d1c7lem1  43421  reelznn0nn  43716  mzpnegmpt  43946  binomcxplemrat  45524  binomcxplemnotnn0  45530  negcncfg  47094  itgsinexplem1  47167  stoweidlem34  47247  stirlinglem5  47291  fourierdlem36  47356  fourierdlem89  47408  fourierdlem90  47409  fourierdlem91  47410  fourierdlem107  47426  etransclem9  47456  etransclem14  47461  etransclem28  47475  etransclem35  47482  etransclem46  47493  resubcnnred  48577  m1modmmod  48637  gpgedgvtx0  49362  gpg3kgrtriex  49390  pgnbgreunbgrlem2lem1  49415  pgnbgreunbgrlem2lem2  49416  0nodd  49470  line2  50067  itschlc0xyqsol  50082