Definition df-neg 11408

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

This definition is referenced by:  negeq  11413  nfnegd  11416  csbnegg  11418  negex  11419  negcl  11421  neg0  11468  negid  11469  negsub  11470  subneg  11471  negneg  11472  negsubdi  11478  renegcli  11483  addeq0  11601  mulneg1  11614  mulsubaddmulsub  11642  ltneg  11678  leneg  11681  ixi  11807  0mnnnnn0  12474  max0sub  13156  fzshftral  13576  bernneq2  14195  discr1  14204  discr  14205  cji  15125  rlimrege0  15545  rlimneg  15613  risefall0lem  15992  fallfacfwd  16002  binomfallfaclem2  16006  fsumcube  16026  divalglem1  16364  divalglem2  16365  m1bits  16410  bitsinv1lem  16411  prmdiv  16755  pcrec  16829  pcid  16844  4sqlem6  16914  4sqlem10  16918  psgnunilem2  19425  cnheibor  24854  evth2  24859  dvlipcn  25899  dvfsumge  25928  ftc2  25951  vieta1lem2  26219  abelthlem8  26349  cospi  26381  coshalfpip  26403  ptolemy  26405  pige3ALT  26429  tanregt0  26448  argimgt0  26521  logcnlem3  26553  logf1o2  26559  advlogexp  26564  logtayl  26569  dvsqrt  26651  dvcnsqrt  26653  cxpcn3  26658  ang180lem3  26721  isosctrlem2  26729  asinlem  26778  atancj  26820  atanlogaddlem  26823  atantan  26833  dvatan  26845  emcllem7  26912  dmgmaddn0  26933  lgamgulmlem5  26943  lgambdd  26947  ftalem3  26985  1sgm2ppw  27111  dchrfi  27166  lgslem4  27211  lgseisen  27290  log2sumbnd  27455  colinearalglem4  28836  re0cj  32667  quad3d  32673  sgnneg  32758  chnub  32938  constrrtcc  33725  constrelextdg2  33737  2sqr3minply  33770  cos9thpiminplylem1  33772  qqhcn  33981  ballotlem1c  34499  quad3  35657  fz0n  35718  climlec3  35721  fwddifnp1  36153  tan2h  37606  broucube  37648  ftc2nc  37696  dvasin  37698  dvacos  37699  areacirclem1  37702  lcmineqlem7  42023  lcmineqlem10  42026  lcmineqlem12  42028  aks4d1p1p7  42062  posbezout  42088  bcle2d  42167  aks6d1c7lem1  42168  reelznn0nn  42449  mzpnegmpt  42732  binomcxplemrat  44339  binomcxplemnotnn0  44345  negcncfg  45879  itgsinexplem1  45952  stoweidlem34  46032  stirlinglem5  46076  fourierdlem36  46141  fourierdlem89  46193  fourierdlem90  46194  fourierdlem91  46195  fourierdlem107  46211  etransclem9  46241  etransclem14  46246  etransclem28  46260  etransclem35  46267  etransclem46  46278  resubcnnred  47305  m1modmmod  47359  gpgedgvtx0  48052  gpg3kgrtriex  48080  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  0nodd  48158  line2  48741  itschlc0xyqsol  48756