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 ⊢ − A = if A = +∞ −∞ if A = −∞ +∞ − A

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 0 cxne class − A
2 cpnf class +∞
3 0 2 wceq wff A = +∞
4 cmnf class −∞
5 0 4 wceq wff A = −∞
6 0 cneg class − A
7 5 2 6 cif class if A = −∞ +∞ − A
8 3 4 7 cif class if A = +∞ −∞ if A = −∞ +∞ − A
9 1 8 wceq wff − A = if A = +∞ −∞ if A = −∞ +∞ − A