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
|- -e -oo = +oo

Proof

Step Hyp Ref Expression
1 df-xneg
 |-  -e -oo = if ( -oo = +oo , -oo , if ( -oo = -oo , +oo , -u -oo ) )
2 mnfnepnf
 |-  -oo =/= +oo
3 ifnefalse
 |-  ( -oo =/= +oo -> if ( -oo = +oo , -oo , if ( -oo = -oo , +oo , -u -oo ) ) = if ( -oo = -oo , +oo , -u -oo ) )
4 2 3 ax-mp
 |-  if ( -oo = +oo , -oo , if ( -oo = -oo , +oo , -u -oo ) ) = if ( -oo = -oo , +oo , -u -oo )
5 eqid
 |-  -oo = -oo
6 5 iftruei
 |-  if ( -oo = -oo , +oo , -u -oo ) = +oo
7 1 4 6 3eqtri
 |-  -e -oo = +oo