This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ − +∞ = −∞