Theorem xnegpnf 12943

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

Assertion

Ref	Expression
xnegpnf	⊢ -𝑒+∞ = -∞

Proof of Theorem xnegpnf

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

Syntax hints:   = wceq 1539  ifcif 4459  +∞cpnf 11006  -∞cmnf 11007  -cneg 11206  -_𝑒cxne 12845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-if 4460  df-xneg 12848

This theorem is referenced by:  xnegcl  12947  xnegneg  12948  xltnegi  12950  xnegid  12972  xnegdi  12982  xaddass2  12984  xsubge0  12995  xlesubadd  12997  xmulneg1  13003  xmulmnf1  13010  xadddi2  13031  xrsdsreclblem  20644  xblss2ps  23554  xblss2  23555  xaddeq0  31076  supminfxr  43004  liminflbuz2  43356