Definition df-neg 11467

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

This definition is referenced by:  negeq  11472  nfnegd  11475  csbnegg  11477  negex  11478  negcl  11480  neg0  11527  negid  11528  negsub  11529  subneg  11530  negneg  11531  negsubdi  11537  renegcli  11542  addeq0  11658  mulneg1  11671  mulsubaddmulsub  11699  ltneg  11735  leneg  11738  ixi  11864  0mnnnnn0  12531  max0sub  13210  fzshftral  13630  bernneq2  14246  discr1  14255  discr  14256  cji  15176  rlimrege0  15593  rlimneg  15661  risefall0lem  16040  fallfacfwd  16050  binomfallfaclem2  16054  fsumcube  16074  divalglem1  16411  divalglem2  16412  m1bits  16457  bitsinv1lem  16458  prmdiv  16802  pcrec  16876  pcid  16891  4sqlem6  16961  4sqlem10  16965  psgnunilem2  19474  cnheibor  24903  evth2  24908  dvlipcn  25949  dvfsumge  25978  ftc2  26001  vieta1lem2  26269  abelthlem8  26399  cospi  26431  coshalfpip  26453  ptolemy  26455  pige3ALT  26479  tanregt0  26498  argimgt0  26571  logcnlem3  26603  logf1o2  26609  advlogexp  26614  logtayl  26619  dvsqrt  26701  dvcnsqrt  26703  cxpcn3  26708  ang180lem3  26771  isosctrlem2  26779  asinlem  26828  atancj  26870  atanlogaddlem  26873  atantan  26883  dvatan  26895  emcllem7  26962  dmgmaddn0  26983  lgamgulmlem5  26993  lgambdd  26997  ftalem3  27035  1sgm2ppw  27161  dchrfi  27216  lgslem4  27261  lgseisen  27340  log2sumbnd  27505  colinearalglem4  28834  re0cj  32667  quad3d  32673  sgnneg  32758  chnub  32938  constrrtcc  33715  constrelextdg2  33727  2sqr3minply  33760  cos9thpiminplylem1  33762  qqhcn  33968  ballotlem1c  34486  quad3  35638  fz0n  35694  climlec3  35697  fwddifnp1  36129  tan2h  37582  broucube  37624  ftc2nc  37672  dvasin  37674  dvacos  37675  areacirclem1  37678  lcmineqlem7  41994  lcmineqlem10  41997  lcmineqlem12  41999  aks4d1p1p7  42033  posbezout  42059  bcle2d  42138  aks6d1c7lem1  42139  reelznn0nn  42439  mzpnegmpt  42714  binomcxplemrat  44322  binomcxplemnotnn0  44328  negcncfg  45858  itgsinexplem1  45931  stoweidlem34  46011  stirlinglem5  46055  fourierdlem36  46120  fourierdlem89  46172  fourierdlem90  46173  fourierdlem91  46174  fourierdlem107  46190  etransclem9  46220  etransclem14  46225  etransclem28  46239  etransclem35  46246  etransclem46  46257  resubcnnred  47281  gpgedgvtx0  48013  gpg3kgrtriex  48039  0nodd  48093  m1modmmod  48449  line2  48680  itschlc0xyqsol  48695