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

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