Definition df-neg 11488

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

This definition is referenced by:  negeq  11493  nfnegd  11496  csbnegg  11498  negex  11499  negcl  11501  neg0  11547  negid  11548  negsub  11549  subneg  11550  negneg  11551  negsubdi  11557  renegcli  11562  addeq0  11678  mulneg1  11691  mulsubaddmulsub  11719  ltneg  11755  leneg  11758  ixi  11884  0mnnnnn0  12550  max0sub  13223  fzshftral  13637  bernneq2  14242  discr1  14251  discr  14252  cji  15159  rlimrege0  15576  rlimneg  15646  risefall0lem  16023  fallfacfwd  16033  binomfallfaclem2  16037  fsumcube  16057  divalglem1  16391  divalglem2  16392  m1bits  16435  bitsinv1lem  16436  prmdiv  16782  pcrec  16855  pcid  16870  4sqlem6  16940  4sqlem10  16944  psgnunilem2  19489  cnheibor  24969  evth2  24974  dvlipcn  26015  dvfsumge  26044  ftc2  26067  vieta1lem2  26336  abelthlem8  26466  cospi  26497  coshalfpip  26519  ptolemy  26521  pige3ALT  26544  tanregt0  26563  argimgt0  26636  logcnlem3  26668  logf1o2  26674  advlogexp  26679  logtayl  26684  dvsqrt  26766  dvcnsqrt  26768  cxpcn3  26773  ang180lem3  26836  isosctrlem2  26844  asinlem  26893  atancj  26935  atanlogaddlem  26938  atantan  26948  dvatan  26960  emcllem7  27027  dmgmaddn0  27048  lgamgulmlem5  27058  lgambdd  27062  ftalem3  27100  1sgm2ppw  27226  dchrfi  27281  lgslem4  27326  lgseisen  27405  log2sumbnd  27570  colinearalglem4  28840  re0cj  32656  quad3d  32657  chnub  32884  constrrtcc  33608  constrelextdg2  33619  2sqr3minply  33620  qqhcn  33819  ballotlem1c  34354  sgnneg  34387  quad3  35511  fz0n  35566  climlec3  35569  fwddifnp1  36002  tan2h  37326  broucube  37368  ftc2nc  37416  dvasin  37418  dvacos  37419  areacirclem1  37422  lcmineqlem7  41747  lcmineqlem10  41750  lcmineqlem12  41752  aks4d1p1p7  41786  posbezout  41812  bcle2d  41891  aks6d1c7lem1  41892  reelznn0nn  42160  mzpnegmpt  42438  binomcxplemrat  44061  binomcxplemnotnn0  44067  negcncfg  45538  itgsinexplem1  45611  stoweidlem34  45691  stirlinglem5  45735  fourierdlem36  45800  fourierdlem89  45852  fourierdlem90  45853  fourierdlem91  45854  fourierdlem107  45870  etransclem9  45900  etransclem14  45905  etransclem28  45919  etransclem35  45926  etransclem46  45937  resubcnnred  46953  0nodd  47583  m1modmmod  47945  line2  48176  itschlc0xyqsol  48191