Metamath Proof Explorer


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 ( 𝐴 = -∞ , +∞ , - 𝐴 ) )