Definition df-neg 11377

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

This definition is referenced by:  negeq  11382  nfnegd  11385  csbnegg  11387  negex  11388  negcl  11390  neg0  11437  negid  11438  negsub  11439  subneg  11440  negneg  11441  negsubdi  11447  renegcli  11452  addeq0  11570  mulneg1  11583  mulsubaddmulsub  11611  ltneg  11647  leneg  11650  ixi  11776  0mnnnnn0  12466  max0sub  13145  fzshftral  13566  bernneq2  14189  discr1  14198  discr  14199  cji  15118  rlimrege0  15538  rlimneg  15606  risefall0lem  15988  fallfacfwd  15998  binomfallfaclem2  16002  fsumcube  16022  divalglem1  16360  divalglem2  16361  m1bits  16406  bitsinv1lem  16407  prmdiv  16752  pcrec  16826  pcid  16841  4sqlem6  16911  4sqlem10  16915  chnub  18585  psgnunilem2  19467  cnheibor  24919  evth2  24924  dvlipcn  25958  dvfsumge  25986  ftc2  26008  vieta1lem2  26274  abelthlem8  26401  cospi  26433  coshalfpip  26455  ptolemy  26457  pige3ALT  26481  tanregt0  26500  argimgt0  26573  logcnlem3  26605  logf1o2  26611  advlogexp  26616  logtayl  26621  dvsqrt  26703  dvcnsqrt  26705  cxpcn3  26709  ang180lem3  26772  isosctrlem2  26780  asinlem  26829  atancj  26871  atanlogaddlem  26874  atantan  26884  dvatan  26896  emcllem7  26962  dmgmaddn0  26983  lgamgulmlem5  26993  lgambdd  26997  ftalem3  27035  1sgm2ppw  27160  dchrfi  27215  lgslem4  27260  lgseisen  27339  log2sumbnd  27504  colinearalglem4  28975  re0cj  32813  quad3d  32819  sgnneg  32903  constrrtcc  33876  constrelextdg2  33888  2sqr3minply  33921  cos9thpiminplylem1  33923  qqhcn  34132  ballotlem1c  34649  quad3  35849  fz0n  35910  climlec3  35913  fwddifnp1  36344  qdiff  37638  tan2h  37930  broucube  37972  ftc2nc  38020  dvasin  38022  dvacos  38023  areacirclem1  38026  lcmineqlem7  42471  lcmineqlem10  42474  lcmineqlem12  42476  aks4d1p1p7  42510  posbezout  42536  bcle2d  42615  aks6d1c7lem1  42616  reelznn0nn  42903  mzpnegmpt  43173  binomcxplemrat  44774  binomcxplemnotnn0  44780  negcncfg  46306  itgsinexplem1  46379  stoweidlem34  46459  stirlinglem5  46503  fourierdlem36  46568  fourierdlem89  46620  fourierdlem90  46621  fourierdlem91  46622  fourierdlem107  46638  etransclem9  46668  etransclem14  46673  etransclem28  46687  etransclem35  46694  etransclem46  46705  nthrucw  47311  resubcnnred  47743  m1modmmod  47803  gpgedgvtx0  48528  gpg3kgrtriex  48556  pgnbgreunbgrlem2lem1  48581  pgnbgreunbgrlem2lem2  48582  0nodd  48637  line2  49219  itschlc0xyqsol  49234