Definition df-xneg

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

	Ref	Expression
Assertion	df-xneg	⊢ -𝑒 𝐴 = if ( 𝐴 = +∞ , -∞ , if ( 𝐴 = -∞ , +∞ , - 𝐴 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1	0	cxne	⊢ -𝑒 𝐴
2		cpnf	⊢ +∞
3	0 2	wceq	⊢ 𝐴 = +∞
4		cmnf	⊢ -∞
5	0 4	wceq	⊢ 𝐴 = -∞
6	0	cneg	⊢ - 𝐴
7	5 2 6	cif	⊢ if ( 𝐴 = -∞ , +∞ , - 𝐴 )
8	3 4 7	cif	⊢ if ( 𝐴 = +∞ , -∞ , if ( 𝐴 = -∞ , +∞ , - 𝐴 ) )
9	1 8	wceq	⊢ -𝑒 𝐴 = if ( 𝐴 = +∞ , -∞ , if ( 𝐴 = -∞ , +∞ , - 𝐴 ) )