Definition df-neg 11523

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

This definition is referenced by:  negeq  11528  nfnegd  11531  csbnegg  11533  negex  11534  negcl  11536  neg0  11582  negid  11583  negsub  11584  subneg  11585  negneg  11586  negsubdi  11592  renegcli  11597  addeq0  11713  mulneg1  11726  mulsubaddmulsub  11754  ltneg  11790  leneg  11793  ixi  11919  0mnnnnn0  12585  max0sub  13258  fzshftral  13672  bernneq2  14279  discr1  14288  discr  14289  cji  15208  rlimrege0  15625  rlimneg  15695  risefall0lem  16074  fallfacfwd  16084  binomfallfaclem2  16088  fsumcube  16108  divalglem1  16442  divalglem2  16443  m1bits  16486  bitsinv1lem  16487  prmdiv  16832  pcrec  16905  pcid  16920  4sqlem6  16990  4sqlem10  16994  psgnunilem2  19537  cnheibor  25006  evth2  25011  dvlipcn  26053  dvfsumge  26082  ftc2  26105  vieta1lem2  26371  abelthlem8  26501  cospi  26532  coshalfpip  26554  ptolemy  26556  pige3ALT  26580  tanregt0  26599  argimgt0  26672  logcnlem3  26704  logf1o2  26710  advlogexp  26715  logtayl  26720  dvsqrt  26802  dvcnsqrt  26804  cxpcn3  26809  ang180lem3  26872  isosctrlem2  26880  asinlem  26929  atancj  26971  atanlogaddlem  26974  atantan  26984  dvatan  26996  emcllem7  27063  dmgmaddn0  27084  lgamgulmlem5  27094  lgambdd  27098  ftalem3  27136  1sgm2ppw  27262  dchrfi  27317  lgslem4  27362  lgseisen  27441  log2sumbnd  27606  colinearalglem4  28942  re0cj  32756  quad3d  32757  chnub  32984  constrrtcc  33726  constrelextdg2  33737  2sqr3minply  33738  qqhcn  33937  ballotlem1c  34472  sgnneg  34505  quad3  35638  fz0n  35693  climlec3  35696  fwddifnp1  36129  tan2h  37572  broucube  37614  ftc2nc  37662  dvasin  37664  dvacos  37665  areacirclem1  37668  lcmineqlem7  41992  lcmineqlem10  41995  lcmineqlem12  41997  aks4d1p1p7  42031  posbezout  42057  bcle2d  42136  aks6d1c7lem1  42137  reelznn0nn  42425  mzpnegmpt  42700  binomcxplemrat  44319  binomcxplemnotnn0  44325  negcncfg  45802  itgsinexplem1  45875  stoweidlem34  45955  stirlinglem5  45999  fourierdlem36  46064  fourierdlem89  46116  fourierdlem90  46117  fourierdlem91  46118  fourierdlem107  46134  etransclem9  46164  etransclem14  46169  etransclem28  46183  etransclem35  46190  etransclem46  46201  resubcnnred  47219  0nodd  47893  m1modmmod  48255  line2  48486  itschlc0xyqsol  48501