Definition df-neg 11369

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

This definition is referenced by:  negeq  11374  nfnegd  11377  csbnegg  11379  negex  11380  negcl  11382  neg0  11429  negid  11430  negsub  11431  subneg  11432  negneg  11433  negsubdi  11439  renegcli  11444  addeq0  11562  mulneg1  11575  mulsubaddmulsub  11603  ltneg  11639  leneg  11642  ixi  11768  0mnnnnn0  12458  max0sub  13137  fzshftral  13558  bernneq2  14181  discr1  14190  discr  14191  cji  15110  rlimrege0  15530  rlimneg  15598  risefall0lem  15980  fallfacfwd  15990  binomfallfaclem2  15994  fsumcube  16014  divalglem1  16352  divalglem2  16353  m1bits  16398  bitsinv1lem  16399  prmdiv  16744  pcrec  16818  pcid  16833  4sqlem6  16903  4sqlem10  16907  chnub  18577  psgnunilem2  19459  cnheibor  24910  evth2  24915  dvlipcn  25949  dvfsumge  25977  ftc2  25999  vieta1lem2  26265  abelthlem8  26392  cospi  26424  coshalfpip  26446  ptolemy  26448  pige3ALT  26472  tanregt0  26491  argimgt0  26564  logcnlem3  26596  logf1o2  26602  advlogexp  26607  logtayl  26612  dvsqrt  26694  dvcnsqrt  26696  cxpcn3  26700  ang180lem3  26763  isosctrlem2  26771  asinlem  26820  atancj  26862  atanlogaddlem  26865  atantan  26875  dvatan  26887  emcllem7  26953  dmgmaddn0  26974  lgamgulmlem5  26984  lgambdd  26988  ftalem3  27026  1sgm2ppw  27151  dchrfi  27206  lgslem4  27251  lgseisen  27330  log2sumbnd  27495  colinearalglem4  28966  re0cj  32804  quad3d  32810  sgnneg  32894  constrrtcc  33867  constrelextdg2  33879  2sqr3minply  33912  cos9thpiminplylem1  33914  qqhcn  34123  ballotlem1c  34640  quad3  35840  fz0n  35901  climlec3  35904  fwddifnp1  36335  qdiff  37629  tan2h  37921  broucube  37963  ftc2nc  38011  dvasin  38013  dvacos  38014  areacirclem1  38017  lcmineqlem7  42462  lcmineqlem10  42465  lcmineqlem12  42467  aks4d1p1p7  42501  posbezout  42527  bcle2d  42606  aks6d1c7lem1  42607  reelznn0nn  42894  mzpnegmpt  43164  binomcxplemrat  44765  binomcxplemnotnn0  44771  negcncfg  46297  itgsinexplem1  46370  stoweidlem34  46450  stirlinglem5  46494  fourierdlem36  46559  fourierdlem89  46611  fourierdlem90  46612  fourierdlem91  46613  fourierdlem107  46629  etransclem9  46659  etransclem14  46664  etransclem28  46678  etransclem35  46685  etransclem46  46696  nthrucw  47304  resubcnnred  47740  m1modmmod  47800  gpgedgvtx0  48525  gpg3kgrtriex  48553  pgnbgreunbgrlem2lem1  48578  pgnbgreunbgrlem2lem2  48579  0nodd  48634  line2  49216  itschlc0xyqsol  49231