Definition df-neg 5338

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 5273 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 5273	. 2 class -uA
3		cc0 5214	. . 3 class 0
4		cmin 5272	. . 3 class -
5	3, 1, 4	co 3954	. 2 class (0 - A)
6	2, 5	wceq 954	1 wff -uA = (0 - A)

This definition is referenced by:  negeq 5339  hbneg 5342  negex 5345  negclt 5348  negidt 5359  neg11 5386  neg0 5395  renegcl 5396  mulneg1 5425  eqneg 5768  nn0subt 6116  fzshftralt 6462  seq0seqz 6482  seq00 6490  bernneq2 6592  discrlem3 6596  sqrlem11 6621  cji 6770  bcpasc 6915  fsumshft 6977  climrecl 7055  addinv 8080  cospi 8620  coshalfpip 8637  pilog 8707  nlelch 9932

Copyright terms: Public domain