Definition df-neg 11492

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

This definition is referenced by:  negeq  11497  nfnegd  11500  csbnegg  11502  negex  11503  negcl  11505  neg0  11552  negid  11553  negsub  11554  subneg  11555  negneg  11556  negsubdi  11562  renegcli  11567  addeq0  11683  mulneg1  11696  mulsubaddmulsub  11724  ltneg  11760  leneg  11763  ixi  11889  0mnnnnn0  12555  max0sub  13234  fzshftral  13651  bernneq2  14265  discr1  14274  discr  14275  cji  15194  rlimrege0  15611  rlimneg  15679  risefall0lem  16058  fallfacfwd  16068  binomfallfaclem2  16072  fsumcube  16092  divalglem1  16427  divalglem2  16428  m1bits  16473  bitsinv1lem  16474  prmdiv  16818  pcrec  16891  pcid  16906  4sqlem6  16976  4sqlem10  16980  psgnunilem2  19527  cnheibor  25000  evth2  25005  dvlipcn  26047  dvfsumge  26076  ftc2  26099  vieta1lem2  26367  abelthlem8  26497  cospi  26528  coshalfpip  26550  ptolemy  26552  pige3ALT  26576  tanregt0  26595  argimgt0  26668  logcnlem3  26700  logf1o2  26706  advlogexp  26711  logtayl  26716  dvsqrt  26798  dvcnsqrt  26800  cxpcn3  26805  ang180lem3  26868  isosctrlem2  26876  asinlem  26925  atancj  26967  atanlogaddlem  26970  atantan  26980  dvatan  26992  emcllem7  27059  dmgmaddn0  27080  lgamgulmlem5  27090  lgambdd  27094  ftalem3  27132  1sgm2ppw  27258  dchrfi  27313  lgslem4  27358  lgseisen  27437  log2sumbnd  27602  colinearalglem4  28938  re0cj  32759  quad3d  32760  chnub  32985  constrrtcc  33740  constrelextdg2  33751  2sqr3minply  33752  qqhcn  33953  ballotlem1c  34488  sgnneg  34521  quad3  35654  fz0n  35710  climlec3  35713  fwddifnp1  36146  tan2h  37598  broucube  37640  ftc2nc  37688  dvasin  37690  dvacos  37691  areacirclem1  37694  lcmineqlem7  42016  lcmineqlem10  42019  lcmineqlem12  42021  aks4d1p1p7  42055  posbezout  42081  bcle2d  42160  aks6d1c7lem1  42161  reelznn0nn  42455  mzpnegmpt  42731  binomcxplemrat  44345  binomcxplemnotnn0  44351  negcncfg  45836  itgsinexplem1  45909  stoweidlem34  45989  stirlinglem5  46033  fourierdlem36  46098  fourierdlem89  46150  fourierdlem90  46151  fourierdlem91  46152  fourierdlem107  46168  etransclem9  46198  etransclem14  46203  etransclem28  46217  etransclem35  46224  etransclem46  46235  resubcnnred  47253  gpgedgvtx0  47953  0nodd  48013  m1modmmod  48370  line2  48601  itschlc0xyqsol  48616