Definition df-neg 11365

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

This definition is referenced by:  negeq  11370  nfnegd  11373  csbnegg  11375  negex  11376  negcl  11378  neg0  11425  negid  11426  negsub  11427  subneg  11428  negneg  11429  negsubdi  11435  renegcli  11440  addeq0  11558  mulneg1  11571  mulsubaddmulsub  11599  ltneg  11635  leneg  11638  ixi  11764  0mnnnnn0  12431  max0sub  13109  fzshftral  13529  bernneq2  14151  discr1  14160  discr  14161  cji  15080  rlimrege0  15500  rlimneg  15568  risefall0lem  15947  fallfacfwd  15957  binomfallfaclem2  15961  fsumcube  15981  divalglem1  16319  divalglem2  16320  m1bits  16365  bitsinv1lem  16366  prmdiv  16710  pcrec  16784  pcid  16799  4sqlem6  16869  4sqlem10  16873  chnub  18543  psgnunilem2  19422  cnheibor  24908  evth2  24913  dvlipcn  25953  dvfsumge  25982  ftc2  26005  vieta1lem2  26273  abelthlem8  26403  cospi  26435  coshalfpip  26457  ptolemy  26459  pige3ALT  26483  tanregt0  26502  argimgt0  26575  logcnlem3  26607  logf1o2  26613  advlogexp  26618  logtayl  26623  dvsqrt  26705  dvcnsqrt  26707  cxpcn3  26712  ang180lem3  26775  isosctrlem2  26783  asinlem  26832  atancj  26874  atanlogaddlem  26877  atantan  26887  dvatan  26899  emcllem7  26966  dmgmaddn0  26987  lgamgulmlem5  26997  lgambdd  27001  ftalem3  27039  1sgm2ppw  27165  dchrfi  27220  lgslem4  27265  lgseisen  27344  log2sumbnd  27509  colinearalglem4  28931  re0cj  32772  quad3d  32778  sgnneg  32863  constrrtcc  33841  constrelextdg2  33853  2sqr3minply  33886  cos9thpiminplylem1  33888  qqhcn  34097  ballotlem1c  34614  quad3  35813  fz0n  35874  climlec3  35877  fwddifnp1  36308  tan2h  37752  broucube  37794  ftc2nc  37842  dvasin  37844  dvacos  37845  areacirclem1  37848  lcmineqlem7  42228  lcmineqlem10  42231  lcmineqlem12  42233  aks4d1p1p7  42267  posbezout  42293  bcle2d  42372  aks6d1c7lem1  42373  reelznn0nn  42658  mzpnegmpt  42928  binomcxplemrat  44533  binomcxplemnotnn0  44539  negcncfg  46067  itgsinexplem1  46140  stoweidlem34  46220  stirlinglem5  46264  fourierdlem36  46329  fourierdlem89  46381  fourierdlem90  46382  fourierdlem91  46383  fourierdlem107  46399  etransclem9  46429  etransclem14  46434  etransclem28  46448  etransclem35  46455  etransclem46  46466  nthrucw  47072  resubcnnred  47492  m1modmmod  47546  gpgedgvtx0  48249  gpg3kgrtriex  48277  pgnbgreunbgrlem2lem1  48302  pgnbgreunbgrlem2lem2  48303  0nodd  48358  line2  48940  itschlc0xyqsol  48955