Definition df-neg 5330

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 5265 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 5265	. 2 class -uA
3		cc0 5206	. . 3 class 0
4		cmin 5264	. . 3 class -
5	3, 1, 4	co 3948	. 2 class (0 - A)
6	2, 5	wceq 953	1 wff -uA = (0 - A)

This definition is referenced by:  negeq 5331  hbneg 5334  negex 5337  negclt 5340  negidt 5351  neg11 5378  neg0 5387  renegcl 5388  mulneg1 5417  eqneg 5760  nn0subt 6108  fzshftralt 6454  seq0seqz 6474  seq00 6482  bernneq2 6584  discrlem3 6588  sqrlem11 6613  cji 6762  bcpasc 6907  fsumshft 6969  climrecl 7047  addinv 8065  cospi 8601  coshalfpip 8618  pilog 8690  nlelch 9909

Copyright terms: Public domain