Theorem xnegpnf 13108

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 13011	. 2 ⊢ -𝑒+∞ = if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞))
2		eqid 2731	. . 3 ⊢ +∞ = +∞
3	2	iftruei 4479	. 2 ⊢ if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) = -∞
4	1, 3	eqtri 2754	1 ⊢ -𝑒+∞ = -∞

Syntax hints:   = wceq 1541  ifcif 4472  +∞cpnf 11143  -∞cmnf 11144  -cneg 11345  -_𝑒cxne 13008

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-if 4473  df-xneg 13011

This theorem is referenced by:  xnegcl  13112  xnegneg  13113  xltnegi  13115  xnegid  13137  xnegdi  13147  xaddass2  13149  xsubge0  13160  xlesubadd  13162  xmulneg1  13168  xmulmnf1  13175  xadddi2  13196  xrsdsreclblem  21349  xblss2ps  24316  xblss2  24317  xaddeq0  32736  supminfxr  45572  liminflbuz2  45923