Definition df-neg 11469

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

This definition is used by:  negeq  11474  nfnegd  11477  csbnegg  11479  negex  11480  negcl  11482  neg0  11529  negid  11530  negsub  11531  subneg  11532  negneg  11533  negsubdi  11539  renegcli  11544  addeq0  11662  mulneg1  11675  mulsubaddmulsub  11703  ltneg  11739  leneg  11742  ixi  11868  0mnnnnn0  12561  max0sub  13248  fz00m1  13600  fzshftral  13670  bernneq2  14294  discr1  14303  discr  14304  sgnneg  15173  cji  15246  rlimrege0  15666  rlimneg  15734  fallfacfwd  16124  binomfallfaclem2  16128  fsumcube  16148  divalglem1  16486  divalglem2  16487  m1bits  16532  bitsinv1lem  16533  prmdiv  16878  pcrec  16952  pcid  16967  4sqlem6  17037  4sqlem10  17041  chnub  18712  psgnunilem2  19621  cnheibor  25182  evth2  25187  dvlipcn  26221  dvfsumge  26249  ftc2  26271  vieta1lem2  26540  abelthlem8  26670  cospi  26705  coshalfpip  26727  ptolemy  26729  pige3ALT  26753  tanregt0  26772  argimgt0  26845  logcnlem3  26877  logf1o2  26883  advlogexp  26888  logtayl  26893  dvsqrt  26975  dvcnsqrt  26977  cxpcn3  26981  ang180lem3  27044  isosctrlem2  27052  asinlem  27101  atancj  27143  atanlogaddlem  27146  atantan  27156  dvatan  27168  emcllem7  27234  dmgmaddn0  27255  lgamgulmlem5  27265  lgambdd  27269  ftalem3  27307  1sgm2ppw  27432  dchrfi  27487  lgslem4  27532  lgseisen  27611  log2sumbnd  27776  colinearalglem4  29350  re0cj  33199  quad3d  33205  constrrtcc  34230  constrelextdg2  34242  2sqr3minply  34275  cos9thpiminplylem1  34277  qqhcn  34486  ballotlem1c  35004  quad3  36234  fz0n  36295  climlec3  36298  fwddifnp1  36730  qdiff  38064  tan2h  38351  broucube  38388  ftc2nc  38436  dvasin  38438  dvacos  38439  areacirclem1  38442  lcmineqlem7  42886  lcmineqlem10  42889  lcmineqlem12  42891  aks4d1p1p7  42925  posbezout  42951  bcle2d  43030  aks6d1c7lem1  43031  reelznn0nn  43334  mzpnegmpt  43574  binomcxplemrat  45159  binomcxplemnotnn0  45165  negcncfg  46694  itgsinexplem1  46767  stoweidlem34  46847  stirlinglem5  46891  fourierdlem36  46956  fourierdlem89  47008  fourierdlem90  47009  fourierdlem91  47010  fourierdlem107  47026  etransclem9  47056  etransclem14  47061  etransclem28  47075  etransclem35  47082  etransclem46  47093  resubcnnred  48177  m1modmmod  48237  gpgedgvtx0  48962  gpg3kgrtriex  48990  pgnbgreunbgrlem2lem1  49015  pgnbgreunbgrlem2lem2  49016  0nodd  49070  line2  49667  itschlc0xyqsol  49682