Definition df-neg 11350

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

This definition is referenced by:  negeq  11355  nfnegd  11358  csbnegg  11360  negex  11361  negcl  11363  neg0  11410  negid  11411  negsub  11412  subneg  11413  negneg  11414  negsubdi  11420  renegcli  11425  addeq0  11543  mulneg1  11556  mulsubaddmulsub  11584  ltneg  11620  leneg  11623  ixi  11749  0mnnnnn0  12416  max0sub  13098  fzshftral  13518  bernneq2  14137  discr1  14146  discr  14147  cji  15066  rlimrege0  15486  rlimneg  15554  risefall0lem  15933  fallfacfwd  15943  binomfallfaclem2  15947  fsumcube  15967  divalglem1  16305  divalglem2  16306  m1bits  16351  bitsinv1lem  16352  prmdiv  16696  pcrec  16770  pcid  16785  4sqlem6  16855  4sqlem10  16859  psgnunilem2  19374  cnheibor  24852  evth2  24857  dvlipcn  25897  dvfsumge  25926  ftc2  25949  vieta1lem2  26217  abelthlem8  26347  cospi  26379  coshalfpip  26401  ptolemy  26403  pige3ALT  26427  tanregt0  26446  argimgt0  26519  logcnlem3  26551  logf1o2  26557  advlogexp  26562  logtayl  26567  dvsqrt  26649  dvcnsqrt  26651  cxpcn3  26656  ang180lem3  26719  isosctrlem2  26727  asinlem  26776  atancj  26818  atanlogaddlem  26821  atantan  26831  dvatan  26843  emcllem7  26910  dmgmaddn0  26931  lgamgulmlem5  26941  lgambdd  26945  ftalem3  26983  1sgm2ppw  27109  dchrfi  27164  lgslem4  27209  lgseisen  27288  log2sumbnd  27453  colinearalglem4  28854  re0cj  32688  quad3d  32694  sgnneg  32779  chnub  32955  constrrtcc  33708  constrelextdg2  33720  2sqr3minply  33753  cos9thpiminplylem1  33755  qqhcn  33964  ballotlem1c  34482  quad3  35653  fz0n  35714  climlec3  35717  fwddifnp1  36149  tan2h  37602  broucube  37644  ftc2nc  37692  dvasin  37694  dvacos  37695  areacirclem1  37698  lcmineqlem7  42018  lcmineqlem10  42021  lcmineqlem12  42023  aks4d1p1p7  42057  posbezout  42083  bcle2d  42162  aks6d1c7lem1  42163  reelznn0nn  42444  mzpnegmpt  42727  binomcxplemrat  44333  binomcxplemnotnn0  44339  negcncfg  45872  itgsinexplem1  45945  stoweidlem34  46025  stirlinglem5  46069  fourierdlem36  46134  fourierdlem89  46186  fourierdlem90  46187  fourierdlem91  46188  fourierdlem107  46204  etransclem9  46234  etransclem14  46239  etransclem28  46253  etransclem35  46260  etransclem46  46271  resubcnnred  47298  m1modmmod  47352  gpgedgvtx0  48055  gpg3kgrtriex  48083  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  0nodd  48164  line2  48747  itschlc0xyqsol  48762