Definition df-xneg

Description: Define the negative of an extended real number. (Contributed by FL, 26-Dec-2011)

	Ref	Expression
Assertion	df-xneg	|- -e A = if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1	0	cxne	|- -e A
2		cpnf	|- +oo
3	0 2	wceq	|- A = +oo
4		cmnf	|- -oo
5	0 4	wceq	|- A = -oo
6	0	cneg	|- -u A
7	5 2 6	cif	|- if ( A = -oo , +oo , -u A )
8	3 4 7	cif	|- if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) )
9	1 8	wceq	|- -e A = if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) )