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	⊢ -𝑒 -∞ = +∞

Proof

Step	Hyp	Ref	Expression
1		df-xneg	⊢ -𝑒 -∞ = if ( -∞ = +∞ , -∞ , if ( -∞ = -∞ , +∞ , - -∞ ) )
2		mnfnepnf	⊢ -∞ ≠ +∞
3		ifnefalse	⊢ ( -∞ ≠ +∞ → if ( -∞ = +∞ , -∞ , if ( -∞ = -∞ , +∞ , - -∞ ) ) = if ( -∞ = -∞ , +∞ , - -∞ ) )
4	2 3	ax-mp	⊢ if ( -∞ = +∞ , -∞ , if ( -∞ = -∞ , +∞ , - -∞ ) ) = if ( -∞ = -∞ , +∞ , - -∞ )
5		eqid	⊢ -∞ = -∞
6	5	iftruei	⊢ if ( -∞ = -∞ , +∞ , - -∞ ) = +∞
7	1 4 6	3eqtri	⊢ -𝑒 -∞ = +∞