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 | ⊢ -𝑒 -∞ = +∞ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-xneg | ⊢ -𝑒 -∞ = if ( -∞ = +∞ , -∞ , if ( -∞ = -∞ , +∞ , - -∞ ) ) | |
2 | mnfnepnf | ⊢ -∞ ≠ +∞ | |
3 | ifnefalse | ⊢ ( -∞ ≠ +∞ → if ( -∞ = +∞ , -∞ , if ( -∞ = -∞ , +∞ , - -∞ ) ) = if ( -∞ = -∞ , +∞ , - -∞ ) ) | |
4 | 2 3 | ax-mp | ⊢ if ( -∞ = +∞ , -∞ , if ( -∞ = -∞ , +∞ , - -∞ ) ) = if ( -∞ = -∞ , +∞ , - -∞ ) |
5 | eqid | ⊢ -∞ = -∞ | |
6 | 5 | iftruei | ⊢ if ( -∞ = -∞ , +∞ , - -∞ ) = +∞ |
7 | 1 4 6 | 3eqtri | ⊢ -𝑒 -∞ = +∞ |