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