Definition df-neg 11381

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

This definition is referenced by:  negeq  11386  nfnegd  11389  csbnegg  11391  negex  11392  negcl  11394  neg0  11441  negid  11442  negsub  11443  subneg  11444  negneg  11445  negsubdi  11451  renegcli  11456  addeq0  11574  mulneg1  11587  mulsubaddmulsub  11615  ltneg  11651  leneg  11654  ixi  11780  0mnnnnn0  12447  max0sub  13125  fzshftral  13545  bernneq2  14167  discr1  14176  discr  14177  cji  15096  rlimrege0  15516  rlimneg  15584  risefall0lem  15963  fallfacfwd  15973  binomfallfaclem2  15977  fsumcube  15997  divalglem1  16335  divalglem2  16336  m1bits  16381  bitsinv1lem  16382  prmdiv  16726  pcrec  16800  pcid  16815  4sqlem6  16885  4sqlem10  16889  chnub  18559  psgnunilem2  19441  cnheibor  24927  evth2  24932  dvlipcn  25972  dvfsumge  26001  ftc2  26024  vieta1lem2  26292  abelthlem8  26422  cospi  26454  coshalfpip  26476  ptolemy  26478  pige3ALT  26502  tanregt0  26521  argimgt0  26594  logcnlem3  26626  logf1o2  26632  advlogexp  26637  logtayl  26642  dvsqrt  26724  dvcnsqrt  26726  cxpcn3  26731  ang180lem3  26794  isosctrlem2  26802  asinlem  26851  atancj  26893  atanlogaddlem  26896  atantan  26906  dvatan  26918  emcllem7  26985  dmgmaddn0  27006  lgamgulmlem5  27016  lgambdd  27020  ftalem3  27058  1sgm2ppw  27184  dchrfi  27239  lgslem4  27284  lgseisen  27363  log2sumbnd  27528  colinearalglem4  29000  re0cj  32840  quad3d  32846  sgnneg  32931  constrrtcc  33919  constrelextdg2  33931  2sqr3minply  33964  cos9thpiminplylem1  33966  qqhcn  34175  ballotlem1c  34692  quad3  35892  fz0n  35953  climlec3  35956  fwddifnp1  36387  tan2h  37892  broucube  37934  ftc2nc  37982  dvasin  37984  dvacos  37985  areacirclem1  37988  lcmineqlem7  42434  lcmineqlem10  42437  lcmineqlem12  42439  aks4d1p1p7  42473  posbezout  42499  bcle2d  42578  aks6d1c7lem1  42579  reelznn0nn  42860  mzpnegmpt  43130  binomcxplemrat  44735  binomcxplemnotnn0  44741  negcncfg  46268  itgsinexplem1  46341  stoweidlem34  46421  stirlinglem5  46465  fourierdlem36  46530  fourierdlem89  46582  fourierdlem90  46583  fourierdlem91  46584  fourierdlem107  46600  etransclem9  46630  etransclem14  46635  etransclem28  46649  etransclem35  46656  etransclem46  46667  nthrucw  47273  resubcnnred  47693  m1modmmod  47747  gpgedgvtx0  48450  gpg3kgrtriex  48478  pgnbgreunbgrlem2lem1  48503  pgnbgreunbgrlem2lem2  48504  0nodd  48559  line2  49141  itschlc0xyqsol  49156