Definition df-neg 10471

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

This definition is referenced by:  negeq  10475  nfnegd  10478  csbnegg  10480  negex  10481  negcl  10483  neg0  10529  negid  10530  negsub  10531  subneg  10532  negneg  10533  negsubdi  10539  renegcli  10544  mulneg1  10668  ltneg  10730  leneg  10733  ixi  10858  0mnnnnn0  11527  max0sub  12232  fzshftral  12635  bernneq2  13198  discr1  13207  discr  13208  cji  14107  rlimrege0  14518  rlimneg  14585  risefall0lem  14963  fallfacfwd  14973  binomfallfaclem2  14977  fsumcube  14997  divalglem1  15325  divalglem2  15326  m1bits  15370  bitsinv1lem  15371  prmdiv  15697  pcrec  15770  pcid  15784  4sqlem6  15854  4sqlem10  15858  psgnunilem2  18122  cnheibor  22974  evth2  22979  dvlipcn  23977  dvfsumge  24005  ftc2  24027  vieta1lem2  24286  abelthlem8  24413  cospi  24445  coshalfpip  24467  ptolemy  24469  pige3  24490  tanregt0  24506  argimgt0  24579  logcnlem3  24611  logf1o2  24617  advlogexp  24622  logtayl  24627  dvsqrt  24704  dvcnsqrt  24706  cxpcn3  24710  ang180lem3  24762  isosctrlem2  24770  asinlem  24816  atancj  24858  atanlogaddlem  24861  atantan  24871  dvatan  24883  emcllem7  24949  dmgmaddn0  24970  lgamgulmlem5  24980  lgambdd  24984  ftalem3  25022  1sgm2ppw  25146  dchrfi  25201  lgslem4  25246  lgseisen  25325  log2sumbnd  25454  colinearalglem4  26010  addeq0  29850  qqhcn  30375  ballotlem1c  30909  sgnneg  30942  quad3  31902  fz0n  31954  climlec3  31957  fwddifnp1  32609  tan2h  33734  broucube  33776  ftc2nc  33826  dvasin  33828  dvacos  33829  areacirclem1  33832  mzpnegmpt  37833  binomcxplemrat  39075  binomcxplemnotnn0  39081  negcncfg  40612  itgsinexplem1  40687  stoweidlem34  40768  stirlinglem5  40812  fourierdlem36  40877  fourierdlem89  40929  fourierdlem90  40930  fourierdlem91  40931  fourierdlem107  40947  etransclem9  40977  etransclem14  40982  etransclem28  40996  etransclem35  41003  etransclem46  41014  0nodd  42338  m1modmmod  42844