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  32687  quad3d  32693  sgnneg  32778  chnub  32954  constrrtcc  33702  constrelextdg2  33714  2sqr3minply  33747  cos9thpiminplylem1  33749  qqhcn  33958  ballotlem1c  34476  quad3  35643  fz0n  35704  climlec3  35707  fwddifnp1  36139  tan2h  37592  broucube  37634  ftc2nc  37682  dvasin  37684  dvacos  37685  areacirclem1  37688  lcmineqlem7  42008  lcmineqlem10  42011  lcmineqlem12  42013  aks4d1p1p7  42047  posbezout  42073  bcle2d  42152  aks6d1c7lem1  42153  reelznn0nn  42434  mzpnegmpt  42717  binomcxplemrat  44323  binomcxplemnotnn0  44329  negcncfg  45862  itgsinexplem1  45935  stoweidlem34  46015  stirlinglem5  46059  fourierdlem36  46124  fourierdlem89  46176  fourierdlem90  46177  fourierdlem91  46178  fourierdlem107  46194  etransclem9  46224  etransclem14  46229  etransclem28  46243  etransclem35  46250  etransclem46  46261  resubcnnred  47288  m1modmmod  47342  gpgedgvtx0  48045  gpg3kgrtriex  48073  pgnbgreunbgrlem2lem1  48098  pgnbgreunbgrlem2lem2  48099  0nodd  48154  line2  48737  itschlc0xyqsol  48752