Definition df-neg 11447

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

This definition is referenced by:  negeq  11452  nfnegd  11455  csbnegg  11457  negex  11458  negcl  11460  neg0  11506  negid  11507  negsub  11508  subneg  11509  negneg  11510  negsubdi  11516  renegcli  11521  addeq0  11637  mulneg1  11650  mulsubaddmulsub  11678  ltneg  11714  leneg  11717  ixi  11843  0mnnnnn0  12504  max0sub  13175  fzshftral  13589  bernneq2  14193  discr1  14202  discr  14203  cji  15106  rlimrege0  15523  rlimneg  15593  risefall0lem  15970  fallfacfwd  15980  binomfallfaclem2  15984  fsumcube  16004  divalglem1  16337  divalglem2  16338  m1bits  16381  bitsinv1lem  16382  prmdiv  16718  pcrec  16791  pcid  16806  4sqlem6  16876  4sqlem10  16880  psgnunilem2  19363  cnheibor  24471  evth2  24476  dvlipcn  25511  dvfsumge  25539  ftc2  25561  vieta1lem2  25824  abelthlem8  25951  cospi  25982  coshalfpip  26004  ptolemy  26006  pige3ALT  26029  tanregt0  26048  argimgt0  26120  logcnlem3  26152  logf1o2  26158  advlogexp  26163  logtayl  26168  dvsqrt  26250  dvcnsqrt  26252  cxpcn3  26256  ang180lem3  26316  isosctrlem2  26324  asinlem  26373  atancj  26415  atanlogaddlem  26418  atantan  26428  dvatan  26440  emcllem7  26506  dmgmaddn0  26527  lgamgulmlem5  26537  lgambdd  26541  ftalem3  26579  1sgm2ppw  26703  dchrfi  26758  lgslem4  26803  lgseisen  26882  log2sumbnd  27047  colinearalglem4  28198  qqhcn  33002  ballotlem1c  33537  sgnneg  33570  quad3  34686  fz0n  34731  climlec3  34734  fwddifnp1  35168  tan2h  36528  broucube  36570  ftc2nc  36618  dvasin  36620  dvacos  36621  areacirclem1  36624  lcmineqlem7  40948  lcmineqlem10  40951  lcmineqlem12  40953  aks4d1p1p7  40987  reelznn0nn  41370  mzpnegmpt  41530  binomcxplemrat  43157  binomcxplemnotnn0  43163  negcncfg  44645  itgsinexplem1  44718  stoweidlem34  44798  stirlinglem5  44842  fourierdlem36  44907  fourierdlem89  44959  fourierdlem90  44960  fourierdlem91  44961  fourierdlem107  44977  etransclem9  45007  etransclem14  45012  etransclem28  45026  etransclem35  45033  etransclem46  45044  resubcnnred  46060  0nodd  46628  m1modmmod  47255  line2  47486  itschlc0xyqsol  47501