Metamath Proof Explorer


Theorem xnegpnf

Description: Minus +oo . Remark of BourbakiTop1 p. IV.15. (Contributed by FL, 26-Dec-2011)

Ref Expression
Assertion xnegpnf +∞=−∞

Proof

Step Hyp Ref Expression
1 df-xneg +∞=if+∞=+∞−∞if+∞=−∞+∞+∞
2 eqid +∞=+∞
3 2 iftruei if+∞=+∞−∞if+∞=−∞+∞+∞=−∞
4 1 3 eqtri +∞=−∞