Theorem xnegpnf 13214

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 13116	. 2 ⊢ -𝑒+∞ = if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞))
2		eqid 2764	. . 3 ⊢ +∞ = +∞
3	2	iftruei 4489	. 2 ⊢ if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) = -∞
4	1, 3	eqtri 2787	1 ⊢ -𝑒+∞ = -∞

Syntax hints:   = wceq 1562  ifcif 4482  +∞cpnf 11215  -∞cmnf 11216  -cneg 11417  -_𝑒cxne 13113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-if 4483  df-xneg 13116

This theorem is referenced by:  xnegcl  13218  xnegneg  13219  xltnegi  13221  xnegid  13243  xnegdi  13253  xaddass2  13255  xsubge0  13266  xlesubadd  13268  xmulneg1  13274  xmulmnf1  13281  xadddi2  13302  xrsdsreclblem  21467  xblss2ps  24463  xblss2  24464  xaddeq0  32957  supminfxr  46043  liminflbuz2  46394