Definition df-neg 11544

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

This definition is used by:  negeq  11549  nfnegd  11552  csbnegg  11554  negex  11555  negcl  11557  neg0  11604  negid  11605  negsub  11606  subneg  11607  negneg  11608  negsubdi  11614  renegcli  11619  addeq0  11739  mulneg1  11752  mulsubaddmulsub  11780  ltneg  11816  leneg  11819  ixi  11945  0mnnnnn0  12638  max0sub  13326  fz00m1  13679  fzshftral  13749  bernneq2  14374  discr1  14383  discr  14384  sgnneg  15253  cji  15326  rlimrege0  15746  rlimneg  15814  fallfacfwd  16202  binomfallfaclem2  16206  fsumcube  16226  divalglem1  16564  divalglem2  16565  m1bits  16610  bitsinv1lem  16611  prmdiv  16962  pcrec  17036  pcid  17051  4sqlem6  17121  4sqlem10  17125  chnub  18796  psgnunilem2  19709  cnheibor  25276  evth2  25281  dvlipcn  26314  dvfsumge  26342  ftc2  26364  vieta1lem2  26634  abelthlem8  26766  cospi  26801  coshalfpip  26823  ptolemy  26825  pige3ALT  26848  tanregt0  26867  argimgt0  26940  logcnlem3  26972  logf1o2  26978  advlogexp  26983  logtayl  26988  dvsqrt  27070  dvcnsqrt  27072  cxpcn3  27076  ang180lem3  27139  isosctrlem2  27147  asinlem  27196  atancj  27238  atanlogaddlem  27241  atantan  27251  dvatan  27263  emcllem7  27329  dmgmaddn0  27350  lgamgulmlem5  27360  lgambdd  27364  ftalem3  27402  1sgm2ppw  27527  dchrfi  27582  lgslem4  27627  lgseisen  27706  log2sumbnd  27871  colinearalglem4  29487  re0cj  33335  quad3d  33341  constrrtcc  34367  constrelextdg2  34379  2sqr3minply  34412  cos9thpiminplylem1  34414  qqhcn  34623  ballotlem1c  35140  quad3  36435  fz0n  36496  climlec3  36499  fwddifnp1  36930  qdiff  38249  tan2h  38536  broucube  38573  ftc2nc  38621  dvasin  38623  dvacos  38624  areacirclem1  38627  lcmineqlem7  43086  lcmineqlem10  43089  lcmineqlem12  43091  aks4d1p1p7  43125  posbezout  43151  bcle2d  43230  aks6d1c7lem1  43231  reelznn0nn  43526  mzpnegmpt  43755  binomcxplemrat  45334  binomcxplemnotnn0  45340  negcncfg  46891  itgsinexplem1  46964  stoweidlem34  47044  stirlinglem5  47088  fourierdlem36  47153  fourierdlem89  47205  fourierdlem90  47206  fourierdlem91  47207  fourierdlem107  47223  etransclem9  47253  etransclem14  47258  etransclem28  47272  etransclem35  47279  etransclem46  47290  resubcnnred  48374  m1modmmod  48434  gpgedgvtx0  49159  gpg3kgrtriex  49187  pgnbgreunbgrlem2lem1  49212  pgnbgreunbgrlem2lem2  49213  0nodd  49267  line2  49864  itschlc0xyqsol  49879