Description: Define the negative of an extended real number. (Contributed by FL, 26-Dec-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | df-xneg | ⊢ -𝑒 𝐴 = if ( 𝐴 = +∞ , -∞ , if ( 𝐴 = -∞ , +∞ , - 𝐴 ) ) |
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 ( 𝐴 = -∞ , +∞ , - 𝐴 ) ) |