Definition df-neg 11384

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

This definition is referenced by:  negeq  11389  nfnegd  11392  csbnegg  11394  negex  11395  negcl  11397  neg0  11444  negid  11445  negsub  11446  subneg  11447  negneg  11448  negsubdi  11454  renegcli  11459  addeq0  11577  mulneg1  11590  mulsubaddmulsub  11618  ltneg  11654  leneg  11657  ixi  11783  0mnnnnn0  12450  max0sub  13132  fzshftral  13552  bernneq2  14171  discr1  14180  discr  14181  cji  15101  rlimrege0  15521  rlimneg  15589  risefall0lem  15968  fallfacfwd  15978  binomfallfaclem2  15982  fsumcube  16002  divalglem1  16340  divalglem2  16341  m1bits  16386  bitsinv1lem  16387  prmdiv  16731  pcrec  16805  pcid  16820  4sqlem6  16890  4sqlem10  16894  psgnunilem2  19409  cnheibor  24887  evth2  24892  dvlipcn  25932  dvfsumge  25961  ftc2  25984  vieta1lem2  26252  abelthlem8  26382  cospi  26414  coshalfpip  26436  ptolemy  26438  pige3ALT  26462  tanregt0  26481  argimgt0  26554  logcnlem3  26586  logf1o2  26592  advlogexp  26597  logtayl  26602  dvsqrt  26684  dvcnsqrt  26686  cxpcn3  26691  ang180lem3  26754  isosctrlem2  26762  asinlem  26811  atancj  26853  atanlogaddlem  26856  atantan  26866  dvatan  26878  emcllem7  26945  dmgmaddn0  26966  lgamgulmlem5  26976  lgambdd  26980  ftalem3  27018  1sgm2ppw  27144  dchrfi  27199  lgslem4  27244  lgseisen  27323  log2sumbnd  27488  colinearalglem4  28889  re0cj  32717  quad3d  32723  sgnneg  32808  chnub  32984  constrrtcc  33718  constrelextdg2  33730  2sqr3minply  33763  cos9thpiminplylem1  33765  qqhcn  33974  ballotlem1c  34492  quad3  35650  fz0n  35711  climlec3  35714  fwddifnp1  36146  tan2h  37599  broucube  37641  ftc2nc  37689  dvasin  37691  dvacos  37692  areacirclem1  37695  lcmineqlem7  42016  lcmineqlem10  42019  lcmineqlem12  42021  aks4d1p1p7  42055  posbezout  42081  bcle2d  42160  aks6d1c7lem1  42161  reelznn0nn  42442  mzpnegmpt  42725  binomcxplemrat  44332  binomcxplemnotnn0  44338  negcncfg  45872  itgsinexplem1  45945  stoweidlem34  46025  stirlinglem5  46069  fourierdlem36  46134  fourierdlem89  46186  fourierdlem90  46187  fourierdlem91  46188  fourierdlem107  46204  etransclem9  46234  etransclem14  46239  etransclem28  46253  etransclem35  46260  etransclem46  46271  resubcnnred  47298  m1modmmod  47352  gpgedgvtx0  48045  gpg3kgrtriex  48073  pgnbgreunbgrlem2lem1  48097  pgnbgreunbgrlem2lem2  48098  0nodd  48151  line2  48734  itschlc0xyqsol  48749