Theorem xnegpnf 13225

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 13128	. 2 ⊢ -𝑒+∞ = if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞))
2		eqid 2735	. . 3 ⊢ +∞ = +∞
3	2	iftruei 4507	. 2 ⊢ if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) = -∞
4	1, 3	eqtri 2758	1 ⊢ -𝑒+∞ = -∞

Syntax hints:   = wceq 1540  ifcif 4500  +∞cpnf 11266  -∞cmnf 11267  -cneg 11467  -_𝑒cxne 13125

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-if 4501  df-xneg 13128

This theorem is referenced by:  xnegcl  13229  xnegneg  13230  xltnegi  13232  xnegid  13254  xnegdi  13264  xaddass2  13266  xsubge0  13277  xlesubadd  13279  xmulneg1  13285  xmulmnf1  13292  xadddi2  13313  xrsdsreclblem  21380  xblss2ps  24340  xblss2  24341  xaddeq0  32730  supminfxr  45491  liminflbuz2  45844