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