Step |
Hyp |
Ref |
Expression |
1 |
|
df-xneg |
|- -e A = if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) ) |
2 |
|
renepnf |
|- ( A e. RR -> A =/= +oo ) |
3 |
|
ifnefalse |
|- ( A =/= +oo -> if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) ) = if ( A = -oo , +oo , -u A ) ) |
4 |
2 3
|
syl |
|- ( A e. RR -> if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) ) = if ( A = -oo , +oo , -u A ) ) |
5 |
|
renemnf |
|- ( A e. RR -> A =/= -oo ) |
6 |
|
ifnefalse |
|- ( A =/= -oo -> if ( A = -oo , +oo , -u A ) = -u A ) |
7 |
5 6
|
syl |
|- ( A e. RR -> if ( A = -oo , +oo , -u A ) = -u A ) |
8 |
4 7
|
eqtrd |
|- ( A e. RR -> if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) ) = -u A ) |
9 |
1 8
|
eqtrid |
|- ( A e. RR -> -e A = -u A ) |