Definition df-neg 11443

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

This definition is referenced by:  negeq  11448  nfnegd  11451  csbnegg  11453  negex  11454  negcl  11456  neg0  11503  negid  11504  negsub  11505  subneg  11506  negneg  11507  negsubdi  11513  renegcli  11518  addeq0  11636  mulneg1  11649  mulsubaddmulsub  11677  ltneg  11713  leneg  11716  ixi  11842  0mnnnnn0  12535  max0sub  13221  fzshftral  13642  bernneq2  14265  discr1  14274  discr  14275  sgnneg  15136  cji  15209  rlimrege0  15629  rlimneg  15697  risefall0lem  16079  fallfacfwd  16089  binomfallfaclem2  16093  fsumcube  16113  divalglem1  16451  divalglem2  16452  m1bits  16497  bitsinv1lem  16498  prmdiv  16843  pcrec  16917  pcid  16932  4sqlem6  17002  4sqlem10  17006  chnub  18677  psgnunilem2  19564  cnheibor  25093  evth2  25098  dvlipcn  26132  dvfsumge  26160  ftc2  26182  vieta1lem2  26451  abelthlem8  26578  cospi  26613  coshalfpip  26635  ptolemy  26637  pige3ALT  26661  tanregt0  26680  argimgt0  26753  logcnlem3  26785  logf1o2  26791  advlogexp  26796  logtayl  26801  dvsqrt  26883  dvcnsqrt  26885  cxpcn3  26889  ang180lem3  26952  isosctrlem2  26960  asinlem  27009  atancj  27051  atanlogaddlem  27054  atantan  27064  dvatan  27076  emcllem7  27142  dmgmaddn0  27163  lgamgulmlem5  27173  lgambdd  27177  ftalem3  27215  1sgm2ppw  27340  dchrfi  27395  lgslem4  27440  lgseisen  27519  log2sumbnd  27684  colinearalglem4  29225  re0cj  33054  quad3d  33060  constrrtcc  34091  constrelextdg2  34103  2sqr3minply  34136  cos9thpiminplylem1  34138  qqhcn  34347  ballotlem1c  34864  quad3  36116  fz0n  36177  climlec3  36180  fwddifnp1  36611  qdiff  37915  tan2h  38207  broucube  38249  ftc2nc  38297  dvasin  38299  dvacos  38300  areacirclem1  38303  lcmineqlem7  42748  lcmineqlem10  42751  lcmineqlem12  42753  aks4d1p1p7  42787  posbezout  42813  bcle2d  42892  aks6d1c7lem1  42893  reelznn0nn  43181  mzpnegmpt  43423  binomcxplemrat  45008  binomcxplemnotnn0  45014  negcncfg  46543  itgsinexplem1  46616  stoweidlem34  46696  stirlinglem5  46740  fourierdlem36  46805  fourierdlem89  46857  fourierdlem90  46858  fourierdlem91  46859  fourierdlem107  46875  etransclem9  46905  etransclem14  46910  etransclem28  46924  etransclem35  46931  etransclem46  46942  nthrucw  47550  resubcnnred  47986  m1modmmod  48046  gpgedgvtx0  48771  gpg3kgrtriex  48799  pgnbgreunbgrlem2lem1  48824  pgnbgreunbgrlem2lem2  48825  0nodd  48880  line2  49477  itschlc0xyqsol  49492