Definition df-neg 11347

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

This definition is referenced by:  negeq  11352  nfnegd  11355  csbnegg  11357  negex  11358  negcl  11360  neg0  11407  negid  11408  negsub  11409  subneg  11410  negneg  11411  negsubdi  11417  renegcli  11422  addeq0  11540  mulneg1  11553  mulsubaddmulsub  11581  ltneg  11617  leneg  11620  ixi  11746  0mnnnnn0  12413  max0sub  13095  fzshftral  13515  bernneq2  14137  discr1  14146  discr  14147  cji  15066  rlimrege0  15486  rlimneg  15554  risefall0lem  15933  fallfacfwd  15943  binomfallfaclem2  15947  fsumcube  15967  divalglem1  16305  divalglem2  16306  m1bits  16351  bitsinv1lem  16352  prmdiv  16696  pcrec  16770  pcid  16785  4sqlem6  16855  4sqlem10  16859  chnub  18528  psgnunilem2  19407  cnheibor  24881  evth2  24886  dvlipcn  25926  dvfsumge  25955  ftc2  25978  vieta1lem2  26246  abelthlem8  26376  cospi  26408  coshalfpip  26430  ptolemy  26432  pige3ALT  26456  tanregt0  26475  argimgt0  26548  logcnlem3  26580  logf1o2  26586  advlogexp  26591  logtayl  26596  dvsqrt  26678  dvcnsqrt  26680  cxpcn3  26685  ang180lem3  26748  isosctrlem2  26756  asinlem  26805  atancj  26847  atanlogaddlem  26850  atantan  26860  dvatan  26872  emcllem7  26939  dmgmaddn0  26960  lgamgulmlem5  26970  lgambdd  26974  ftalem3  27012  1sgm2ppw  27138  dchrfi  27193  lgslem4  27238  lgseisen  27317  log2sumbnd  27482  colinearalglem4  28887  re0cj  32727  quad3d  32733  sgnneg  32816  constrrtcc  33748  constrelextdg2  33760  2sqr3minply  33793  cos9thpiminplylem1  33795  qqhcn  34004  ballotlem1c  34521  quad3  35714  fz0n  35775  climlec3  35778  fwddifnp1  36209  tan2h  37662  broucube  37704  ftc2nc  37752  dvasin  37754  dvacos  37755  areacirclem1  37758  lcmineqlem7  42138  lcmineqlem10  42141  lcmineqlem12  42143  aks4d1p1p7  42177  posbezout  42203  bcle2d  42282  aks6d1c7lem1  42283  reelznn0nn  42564  mzpnegmpt  42847  binomcxplemrat  44453  binomcxplemnotnn0  44459  negcncfg  45989  itgsinexplem1  46062  stoweidlem34  46142  stirlinglem5  46186  fourierdlem36  46251  fourierdlem89  46303  fourierdlem90  46304  fourierdlem91  46305  fourierdlem107  46321  etransclem9  46351  etransclem14  46356  etransclem28  46370  etransclem35  46377  etransclem46  46388  nthrucw  46994  resubcnnred  47414  m1modmmod  47468  gpgedgvtx0  48171  gpg3kgrtriex  48199  pgnbgreunbgrlem2lem1  48224  pgnbgreunbgrlem2lem2  48225  0nodd  48280  line2  48863  itschlc0xyqsol  48878