Metamath Proof Explorer

Theorem xnegpnf

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

Ref Expression
Assertion xnegpnf 
|- -e +oo = -oo

Proof

Step Hyp Ref Expression
1 df-xneg 
 |-  -e +oo = if ( +oo = +oo , -oo , if ( +oo = -oo , +oo , -u +oo ) )
2 eqid 
 |-  +oo = +oo
3 2 iftruei 
 |-  if ( +oo = +oo , -oo , if ( +oo = -oo , +oo , -u +oo ) ) = -oo
4 1 3 eqtri 
 |-  -e +oo = -oo