Description: Minus +oo . Remark of BourbakiTop1 p. IV.15. (Contributed by FL, 26-Dec-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | xnegpnf | |- -e +oo = -oo |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-xneg | |- -e +oo = if ( +oo = +oo , -oo , if ( +oo = -oo , +oo , -u +oo ) ) |
|
2 | eqid | |- +oo = +oo |
|
3 | 2 | iftruei | |- if ( +oo = +oo , -oo , if ( +oo = -oo , +oo , -u +oo ) ) = -oo |
4 | 1 3 | eqtri | |- -e +oo = -oo |