Definition df-neg 11375

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

This definition is referenced by:  negeq  11380  nfnegd  11383  csbnegg  11385  negex  11386  negcl  11388  neg0  11435  negid  11436  negsub  11437  subneg  11438  negneg  11439  negsubdi  11445  renegcli  11450  addeq0  11568  mulneg1  11581  mulsubaddmulsub  11609  ltneg  11645  leneg  11648  ixi  11774  0mnnnnn0  12464  max0sub  13143  fzshftral  13564  bernneq2  14187  discr1  14196  discr  14197  cji  15116  rlimrege0  15536  rlimneg  15604  risefall0lem  15986  fallfacfwd  15996  binomfallfaclem2  16000  fsumcube  16020  divalglem1  16358  divalglem2  16359  m1bits  16404  bitsinv1lem  16405  prmdiv  16750  pcrec  16824  pcid  16839  4sqlem6  16909  4sqlem10  16913  chnub  18583  psgnunilem2  19465  cnheibor  24944  evth2  24949  dvlipcn  25983  dvfsumge  26011  ftc2  26033  vieta1lem2  26299  abelthlem8  26426  cospi  26458  coshalfpip  26480  ptolemy  26482  pige3ALT  26506  tanregt0  26525  argimgt0  26598  logcnlem3  26630  logf1o2  26636  advlogexp  26641  logtayl  26646  dvsqrt  26728  dvcnsqrt  26730  cxpcn3  26734  ang180lem3  26797  isosctrlem2  26805  asinlem  26854  atancj  26896  atanlogaddlem  26899  atantan  26909  dvatan  26921  emcllem7  26987  dmgmaddn0  27008  lgamgulmlem5  27018  lgambdd  27022  ftalem3  27060  1sgm2ppw  27185  dchrfi  27240  lgslem4  27285  lgseisen  27364  log2sumbnd  27529  colinearalglem4  29000  re0cj  32839  quad3d  32845  sgnneg  32929  constrrtcc  33931  constrelextdg2  33943  2sqr3minply  33976  cos9thpiminplylem1  33978  qqhcn  34187  ballotlem1c  34704  quad3  35913  fz0n  35974  climlec3  35977  fwddifnp1  36408  qdiff  37702  tan2h  37994  broucube  38036  ftc2nc  38084  dvasin  38086  dvacos  38087  areacirclem1  38090  lcmineqlem7  42535  lcmineqlem10  42538  lcmineqlem12  42540  aks4d1p1p7  42574  posbezout  42600  bcle2d  42679  aks6d1c7lem1  42680  reelznn0nn  42966  mzpnegmpt  43208  binomcxplemrat  44809  binomcxplemnotnn0  44815  negcncfg  46338  itgsinexplem1  46411  stoweidlem34  46491  stirlinglem5  46535  fourierdlem36  46600  fourierdlem89  46652  fourierdlem90  46653  fourierdlem91  46654  fourierdlem107  46670  etransclem9  46700  etransclem14  46705  etransclem28  46719  etransclem35  46726  etransclem46  46737  nthrucw  47345  resubcnnred  47781  m1modmmod  47841  gpgedgvtx0  48566  gpg3kgrtriex  48594  pgnbgreunbgrlem2lem1  48619  pgnbgreunbgrlem2lem2  48620  0nodd  48675  line2  49257  itschlc0xyqsol  49272