Definition df-neg 11113

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

This definition is referenced by:  negeq  11118  nfnegd  11121  csbnegg  11123  negex  11124  negcl  11126  neg0  11172  negid  11173  negsub  11174  subneg  11175  negneg  11176  negsubdi  11182  renegcli  11187  addeq0  11303  mulneg1  11316  mulsubaddmulsub  11344  ltneg  11380  leneg  11383  ixi  11509  0mnnnnn0  12170  max0sub  12834  fzshftral  13248  bernneq2  13848  discr1  13857  discr  13858  cji  14773  rlimrege0  15191  rlimneg  15261  risefall0lem  15639  fallfacfwd  15649  binomfallfaclem2  15653  fsumcube  15673  divalglem1  16006  divalglem2  16007  m1bits  16050  bitsinv1lem  16051  prmdiv  16389  pcrec  16462  pcid  16477  4sqlem6  16547  4sqlem10  16551  psgnunilem2  18993  cnheibor  23999  evth2  24004  dvlipcn  25038  dvfsumge  25066  ftc2  25088  vieta1lem2  25351  abelthlem8  25478  cospi  25509  coshalfpip  25531  ptolemy  25533  pige3ALT  25556  tanregt0  25575  argimgt0  25647  logcnlem3  25679  logf1o2  25685  advlogexp  25690  logtayl  25695  dvsqrt  25775  dvcnsqrt  25777  cxpcn3  25781  ang180lem3  25841  isosctrlem2  25849  asinlem  25898  atancj  25940  atanlogaddlem  25943  atantan  25953  dvatan  25965  emcllem7  26031  dmgmaddn0  26052  lgamgulmlem5  26062  lgambdd  26066  ftalem3  26104  1sgm2ppw  26228  dchrfi  26283  lgslem4  26328  lgseisen  26407  log2sumbnd  26572  colinearalglem4  27155  qqhcn  31816  ballotlem1c  32349  sgnneg  32382  quad3  33503  fz0n  33577  climlec3  33580  fwddifnp1  34369  tan2h  35675  broucube  35717  ftc2nc  35765  dvasin  35767  dvacos  35768  areacirclem1  35771  lcmineqlem7  39950  lcmineqlem10  39953  lcmineqlem12  39955  aks4d1p1p7  39988  mzpnegmpt  40454  binomcxplemrat  41830  binomcxplemnotnn0  41836  negcncfg  43285  itgsinexplem1  43358  stoweidlem34  43438  stirlinglem5  43482  fourierdlem36  43547  fourierdlem89  43599  fourierdlem90  43600  fourierdlem91  43601  fourierdlem107  43617  etransclem9  43647  etransclem14  43652  etransclem28  43666  etransclem35  43673  etransclem46  43684  resubcnnred  44657  0nodd  45225  m1modmmod  45728  line2  45959  itschlc0xyqsol  45974