Definition df-neg 5358

Description: Define the negative of a number (unary minus). We use different symbols for unary minus (-u) and subtraction (-) to prevent syntax ambiguity. See cneg 5293 for a discussion of this.

Assertion

Ref	Expression
df-neg	|- -uA = (0 - A)

Detailed syntax breakdown of Definition df-neg

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	cneg 5293	. 2 class -uA
3		cc0 5234	. . 3 class 0
4		cmin 5292	. . 3 class -
5	3, 1, 4	co 3963	. 2 class (0 - A)
6	2, 5	wceq 956	1 wff -uA = (0 - A)

This definition is referenced by:  negeq 5359  hbneg 5362  negex 5365  negclt 5368  negidt 5379  neg11 5406  neg0 5415  renegcl 5416  mulneg1 5445  eqneg 5804  nn0subt 6161  fzshftralt 6522  seq0seqz 6542  seq00 6550  bernneq2 6653  discrlem3 6658  sqrlem11 6683  cji 6827  bcpasc 6969  fsumshft 7031  climrecl 7110  addinv 8128  cospi 8682  coshalfpip 8701  pilog 8768  nlelch 9994

Copyright terms: Public domain