Definition df-neg 11444

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

This definition is referenced by:  negeq  11449  nfnegd  11452  csbnegg  11454  negex  11455  negcl  11457  neg0  11503  negid  11504  negsub  11505  subneg  11506  negneg  11507  negsubdi  11513  renegcli  11518  addeq0  11634  mulneg1  11647  mulsubaddmulsub  11675  ltneg  11711  leneg  11714  ixi  11840  0mnnnnn0  12501  max0sub  13172  fzshftral  13586  bernneq2  14190  discr1  14199  discr  14200  cji  15103  rlimrege0  15520  rlimneg  15590  risefall0lem  15967  fallfacfwd  15977  binomfallfaclem2  15981  fsumcube  16001  divalglem1  16334  divalglem2  16335  m1bits  16378  bitsinv1lem  16379  prmdiv  16715  pcrec  16788  pcid  16803  4sqlem6  16873  4sqlem10  16877  psgnunilem2  19358  cnheibor  24463  evth2  24468  dvlipcn  25503  dvfsumge  25531  ftc2  25553  vieta1lem2  25816  abelthlem8  25943  cospi  25974  coshalfpip  25996  ptolemy  25998  pige3ALT  26021  tanregt0  26040  argimgt0  26112  logcnlem3  26144  logf1o2  26150  advlogexp  26155  logtayl  26160  dvsqrt  26240  dvcnsqrt  26242  cxpcn3  26246  ang180lem3  26306  isosctrlem2  26314  asinlem  26363  atancj  26405  atanlogaddlem  26408  atantan  26418  dvatan  26430  emcllem7  26496  dmgmaddn0  26517  lgamgulmlem5  26527  lgambdd  26531  ftalem3  26569  1sgm2ppw  26693  dchrfi  26748  lgslem4  26793  lgseisen  26872  log2sumbnd  27037  colinearalglem4  28157  qqhcn  32960  ballotlem1c  33495  sgnneg  33528  quad3  34644  fz0n  34689  climlec3  34692  fwddifnp1  35126  tan2h  36469  broucube  36511  ftc2nc  36559  dvasin  36561  dvacos  36562  areacirclem1  36565  lcmineqlem7  40889  lcmineqlem10  40892  lcmineqlem12  40894  aks4d1p1p7  40928  reelznn0nn  41319  mzpnegmpt  41468  binomcxplemrat  43095  binomcxplemnotnn0  43101  negcncfg  44584  itgsinexplem1  44657  stoweidlem34  44737  stirlinglem5  44781  fourierdlem36  44846  fourierdlem89  44898  fourierdlem90  44899  fourierdlem91  44900  fourierdlem107  44916  etransclem9  44946  etransclem14  44951  etransclem28  44965  etransclem35  44972  etransclem46  44983  resubcnnred  45999  0nodd  46567  m1modmmod  47161  line2  47392  itschlc0xyqsol  47407