Metamath Proof Explorer


Theorem xnegmnf

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 -𝑒 -∞ = +∞

Proof

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 -𝑒 -∞ = +∞