Definition df-xneg

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

	Ref	Expression
Assertion	df-xneg	$$⊢-A=if\left(A=\mathrm{+\infty },\mathrm{-\infty },if\left(A=\mathrm{-\infty },\mathrm{+\infty },-A\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1	0	cxne	$$class\left(-A\right)$$
2		cpnf	$$class\mathrm{+\infty }$$
3	0 2	wceq	$$wffA=\mathrm{+\infty }$$
4		cmnf	$$class\mathrm{-\infty }$$
5	0 4	wceq	$$wffA=\mathrm{-\infty }$$
6	0	cneg	$$class\left(-A\right)$$
7	5 2 6	cif	$$classif\left(A=\mathrm{-\infty },\mathrm{+\infty },-A\right)$$
8	3 4 7	cif	$$classif\left(A=\mathrm{+\infty },\mathrm{-\infty },if\left(A=\mathrm{-\infty },\mathrm{+\infty },-A\right)\right)$$
9	1 8	wceq	$$wff-A=if\left(A=\mathrm{+\infty },\mathrm{-\infty },if\left(A=\mathrm{-\infty },\mathrm{+\infty },-A\right)\right)$$