Definition df-neg 11376

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

This definition is referenced by:  negeq  11381  nfnegd  11384  csbnegg  11386  negex  11387  negcl  11389  neg0  11436  negid  11437  negsub  11438  subneg  11439  negneg  11440  negsubdi  11446  renegcli  11451  addeq0  11569  mulneg1  11582  mulsubaddmulsub  11610  ltneg  11646  leneg  11649  ixi  11775  0mnnnnn0  12464  max0sub  13143  fzshftral  13564  bernneq2  14187  discr1  14196  discr  14197  cji  15116  rlimrege0  15536  rlimneg  15604  risefall0lem  15986  fallfacfwd  15996  binomfallfaclem2  16000  fsumcube  16020  divalglem1  16358  divalglem2  16359  m1bits  16404  bitsinv1lem  16405  prmdiv  16750  pcrec  16824  pcid  16839  4sqlem6  16909  4sqlem10  16913  chnub  18583  psgnunilem2  19464  cnheibor  24943  evth2  24948  dvlipcn  25982  dvfsumge  26010  ftc2  26032  vieta1lem2  26298  abelthlem8  26425  cospi  26457  coshalfpip  26479  ptolemy  26481  pige3ALT  26505  tanregt0  26524  argimgt0  26597  logcnlem3  26629  logf1o2  26635  advlogexp  26640  logtayl  26645  dvsqrt  26727  dvcnsqrt  26729  cxpcn3  26733  ang180lem3  26796  isosctrlem2  26804  asinlem  26853  atancj  26895  atanlogaddlem  26898  atantan  26908  dvatan  26920  emcllem7  26986  dmgmaddn0  27007  lgamgulmlem5  27017  lgambdd  27021  ftalem3  27059  1sgm2ppw  27184  dchrfi  27239  lgslem4  27284  lgseisen  27363  log2sumbnd  27528  colinearalglem4  28998  re0cj  32837  quad3d  32843  sgnneg  32927  constrrtcc  33929  constrelextdg2  33941  2sqr3minply  33974  cos9thpiminplylem1  33976  qqhcn  34185  ballotlem1c  34702  quad3  35911  fz0n  35972  climlec3  35975  fwddifnp1  36406  qdiff  37700  tan2h  37992  broucube  38034  ftc2nc  38082  dvasin  38084  dvacos  38085  areacirclem1  38088  lcmineqlem7  42533  lcmineqlem10  42536  lcmineqlem12  42538  aks4d1p1p7  42572  posbezout  42598  bcle2d  42677  aks6d1c7lem1  42678  reelznn0nn  42964  mzpnegmpt  43206  binomcxplemrat  44807  binomcxplemnotnn0  44813  negcncfg  46336  itgsinexplem1  46409  stoweidlem34  46489  stirlinglem5  46533  fourierdlem36  46598  fourierdlem89  46650  fourierdlem90  46651  fourierdlem91  46652  fourierdlem107  46668  etransclem9  46698  etransclem14  46703  etransclem28  46717  etransclem35  46724  etransclem46  46735  nthrucw  47343  resubcnnred  47779  m1modmmod  47839  gpgedgvtx0  48564  gpg3kgrtriex  48592  pgnbgreunbgrlem2lem1  48617  pgnbgreunbgrlem2lem2  48618  0nodd  48673  line2  49255  itschlc0xyqsol  49270