This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-neg

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 for a discussion of this. (Contributed by NM, 10-Feb-1995)

		Ref	Expression
	Assertion	df-neg	\|- -u A = ( 0 - A )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	\|- A
1	0	cneg	\|- -u A
2		cc0	\|- 0
3		cmin	\|- -
4	2 0 3	co	\|- ( 0 - A )
5	1 4	wceq	\|- -u A = ( 0 - A )