Definition df-neg 8352

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

This definition is referenced by:  negeq  8371  nfnegd  8374  csbnegg  8376  negcl  8378  neg0  8424  negid  8425  negsub  8426  subneg  8427  negneg  8428  negsubdi  8434  renegcl  8439  mulneg1  8573  ltneg  8641  leneg  8644  ixi  8762  0mnnnnn0  9433  fzshftral  10342  bernneq2  10922  cji  11462  bdtri  11800  m1bits  12520  bitsinv1lem  12521  prmdiv  12806  pcrec  12880  pcid  12896  4sqlem6  12955  4sqlem10  12959  sin0pilem1  15504  cospi  15523  coshalfpip  15545  ptolemy  15547  logbrec  15683  1sgm2ppw  15718  lgslem4  15731  lgseisen  15802