Definition df-neg 11419

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

This definition is referenced by:  negeq  11424  nfnegd  11427  csbnegg  11429  negex  11430  negcl  11432  neg0  11479  negid  11480  negsub  11481  subneg  11482  negneg  11483  negsubdi  11489  renegcli  11494  addeq0  11612  mulneg1  11625  mulsubaddmulsub  11653  ltneg  11689  leneg  11692  ixi  11818  0mnnnnn0  12515  max0sub  13201  fzshftral  13622  bernneq2  14245  discr1  14254  discr  14255  sgnneg  15115  cji  15188  rlimrege0  15608  rlimneg  15676  risefall0lem  16058  fallfacfwd  16068  binomfallfaclem2  16072  fsumcube  16092  divalglem1  16430  divalglem2  16431  m1bits  16476  bitsinv1lem  16477  prmdiv  16822  pcrec  16896  pcid  16911  4sqlem6  16981  4sqlem10  16985  chnub  18656  psgnunilem2  19537  cnheibor  25019  evth2  25024  dvlipcn  26058  dvfsumge  26086  ftc2  26108  vieta1lem2  26377  abelthlem8  26504  cospi  26539  coshalfpip  26561  ptolemy  26563  pige3ALT  26587  tanregt0  26606  argimgt0  26679  logcnlem3  26711  logf1o2  26717  advlogexp  26722  logtayl  26727  dvsqrt  26809  dvcnsqrt  26811  cxpcn3  26815  ang180lem3  26878  isosctrlem2  26886  asinlem  26935  atancj  26977  atanlogaddlem  26980  atantan  26990  dvatan  27002  emcllem7  27068  dmgmaddn0  27089  lgamgulmlem5  27099  lgambdd  27103  ftalem3  27141  1sgm2ppw  27266  dchrfi  27321  lgslem4  27366  lgseisen  27445  log2sumbnd  27610  colinearalglem4  29112  re0cj  32947  quad3d  32953  constrrtcc  34034  constrelextdg2  34046  2sqr3minply  34079  cos9thpiminplylem1  34081  qqhcn  34290  ballotlem1c  34807  quad3  36025  fz0n  36086  climlec3  36089  fwddifnp1  36520  qdiff  37824  tan2h  38116  broucube  38158  ftc2nc  38206  dvasin  38208  dvacos  38209  areacirclem1  38212  lcmineqlem7  42657  lcmineqlem10  42660  lcmineqlem12  42662  aks4d1p1p7  42696  posbezout  42722  bcle2d  42801  aks6d1c7lem1  42802  reelznn0nn  43088  mzpnegmpt  43330  binomcxplemrat  44931  binomcxplemnotnn0  44937  negcncfg  46460  itgsinexplem1  46533  stoweidlem34  46613  stirlinglem5  46657  fourierdlem36  46722  fourierdlem89  46774  fourierdlem90  46775  fourierdlem91  46776  fourierdlem107  46792  etransclem9  46822  etransclem14  46827  etransclem28  46841  etransclem35  46848  etransclem46  46859  nthrucw  47467  resubcnnred  47903  m1modmmod  47963  gpgedgvtx0  48688  gpg3kgrtriex  48716  pgnbgreunbgrlem2lem1  48741  pgnbgreunbgrlem2lem2  48742  0nodd  48797  line2  49379  itschlc0xyqsol  49394