Description: Minus -oo . Remark of BourbakiTop1 p. IV.15. (Contributed by FL, 26-Dec-2011) (Revised by Mario Carneiro, 20-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | xnegmnf | |- -e -oo = +oo |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-xneg | |- -e -oo = if ( -oo = +oo , -oo , if ( -oo = -oo , +oo , -u -oo ) ) |
|
2 | mnfnepnf | |- -oo =/= +oo |
|
3 | ifnefalse | |- ( -oo =/= +oo -> if ( -oo = +oo , -oo , if ( -oo = -oo , +oo , -u -oo ) ) = if ( -oo = -oo , +oo , -u -oo ) ) |
|
4 | 2 3 | ax-mp | |- if ( -oo = +oo , -oo , if ( -oo = -oo , +oo , -u -oo ) ) = if ( -oo = -oo , +oo , -u -oo ) |
5 | eqid | |- -oo = -oo |
|
6 | 5 | iftruei | |- if ( -oo = -oo , +oo , -u -oo ) = +oo |
7 | 1 4 6 | 3eqtri | |- -e -oo = +oo |