Theorem xnegpnf

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

	Ref	Expression
Assertion	xnegpnf	⊢ -𝑒 +∞ = -∞

Proof

Step	Hyp	Ref	Expression
1		df-xneg	⊢ -𝑒 +∞ = if ( +∞ = +∞ , -∞ , if ( +∞ = -∞ , +∞ , - +∞ ) )
2		eqid	⊢ +∞ = +∞
3	2	iftruei	⊢ if ( +∞ = +∞ , -∞ , if ( +∞ = -∞ , +∞ , - +∞ ) ) = -∞
4	1 3	eqtri	⊢ -𝑒 +∞ = -∞