Definition df-neg 10148

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

This definition is referenced by:  negeq  10152  nfnegd  10155  csbnegg  10157  negex  10158  negcl  10160  neg0  10206  negid  10207  negsub  10208  subneg  10209  negneg  10210  negsubdi  10216  renegcli  10221  mulneg1  10345  ltneg  10407  leneg  10410  ixi  10535  0mnnnnn0  11202  max0sub  11901  fzshftral  12297  bernneq2  12853  discr1  12862  discr  12863  cji  13747  rlimrege0  14158  rlimneg  14225  risefall0lem  14596  fallfacfwd  14606  binomfallfaclem2  14610  fsumcube  14630  divalglem1  14955  divalglem2  14956  m1bits  15000  bitsinv1lem  15001  prmdiv  15328  pcrec  15401  pcid  15415  4sqlem6  15485  4sqlem10  15489  psgnunilem2  17738  cnheibor  22562  evth2  22567  dvlipcn  23561  dvfsumge  23589  ftc2  23611  vieta1lem2  23870  abelthlem8  23997  cospi  24028  coshalfpip  24050  ptolemy  24052  pige3  24073  tanregt0  24089  argimgt0  24162  logcnlem3  24190  logf1o2  24196  advlogexp  24201  logtayl  24206  dvsqrt  24283  dvcnsqrt  24285  cxpcn3  24289  ang180lem3  24341  isosctrlem2  24349  asinlem  24395  atancj  24437  atanlogaddlem  24440  atantan  24450  dvatan  24462  emcllem7  24528  dmgmaddn0  24549  lgamgulmlem5  24559  lgambdd  24563  ftalem3  24601  1sgm2ppw  24725  dchrfi  24780  lgslem4  24825  lgseisen  24904  log2sumbnd  25033  colinearalglem4  25589  addeq0  28898  qqhcn  29363  ballotlem1c  29896  sgnneg  29929  quad3  30818  fz0n  30869  climlec3  30872  fwddifnp1  31442  tan2h  32571  broucube  32613  ftc2nc  32664  dvasin  32666  dvacos  32667  areacirclem1  32670  mzpnegmpt  36325  binomcxplemrat  37571  binomcxplemnotnn0  37577  negcncfg  38766  itgsinexplem1  38845  stoweidlem34  38927  stirlinglem5  38971  fourierdlem36  39036  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  fourierdlem107  39106  etransclem9  39136  etransclem14  39141  etransclem28  39155  etransclem35  39162  etransclem46  39173  0nodd  41600  m1modmmod  42110