Definition df-neg 11371

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

This definition is referenced by:  negeq  11376  nfnegd  11379  csbnegg  11381  negex  11382  negcl  11384  neg0  11431  negid  11432  negsub  11433  subneg  11434  negneg  11435  negsubdi  11441  renegcli  11446  addeq0  11564  mulneg1  11577  mulsubaddmulsub  11605  ltneg  11641  leneg  11644  ixi  11770  0mnnnnn0  12437  max0sub  13115  fzshftral  13535  bernneq2  14157  discr1  14166  discr  14167  cji  15086  rlimrege0  15506  rlimneg  15574  risefall0lem  15953  fallfacfwd  15963  binomfallfaclem2  15967  fsumcube  15987  divalglem1  16325  divalglem2  16326  m1bits  16371  bitsinv1lem  16372  prmdiv  16716  pcrec  16790  pcid  16805  4sqlem6  16875  4sqlem10  16879  chnub  18549  psgnunilem2  19428  cnheibor  24914  evth2  24919  dvlipcn  25959  dvfsumge  25988  ftc2  26011  vieta1lem2  26279  abelthlem8  26409  cospi  26441  coshalfpip  26463  ptolemy  26465  pige3ALT  26489  tanregt0  26508  argimgt0  26581  logcnlem3  26613  logf1o2  26619  advlogexp  26624  logtayl  26629  dvsqrt  26711  dvcnsqrt  26713  cxpcn3  26718  ang180lem3  26781  isosctrlem2  26789  asinlem  26838  atancj  26880  atanlogaddlem  26883  atantan  26893  dvatan  26905  emcllem7  26972  dmgmaddn0  26993  lgamgulmlem5  27003  lgambdd  27007  ftalem3  27045  1sgm2ppw  27171  dchrfi  27226  lgslem4  27271  lgseisen  27350  log2sumbnd  27515  colinearalglem4  28986  re0cj  32825  quad3d  32831  sgnneg  32916  constrrtcc  33894  constrelextdg2  33906  2sqr3minply  33939  cos9thpiminplylem1  33941  qqhcn  34150  ballotlem1c  34667  quad3  35866  fz0n  35927  climlec3  35930  fwddifnp1  36361  tan2h  37815  broucube  37857  ftc2nc  37905  dvasin  37907  dvacos  37908  areacirclem1  37911  lcmineqlem7  42357  lcmineqlem10  42360  lcmineqlem12  42362  aks4d1p1p7  42396  posbezout  42422  bcle2d  42501  aks6d1c7lem1  42502  reelznn0nn  42783  mzpnegmpt  43053  binomcxplemrat  44658  binomcxplemnotnn0  44664  negcncfg  46192  itgsinexplem1  46265  stoweidlem34  46345  stirlinglem5  46389  fourierdlem36  46454  fourierdlem89  46506  fourierdlem90  46507  fourierdlem91  46508  fourierdlem107  46524  etransclem9  46554  etransclem14  46559  etransclem28  46573  etransclem35  46580  etransclem46  46591  nthrucw  47197  resubcnnred  47617  m1modmmod  47671  gpgedgvtx0  48374  gpg3kgrtriex  48402  pgnbgreunbgrlem2lem1  48427  pgnbgreunbgrlem2lem2  48428  0nodd  48483  line2  49065  itschlc0xyqsol  49080