Theorem xnegpnf 13122

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 13024	. 2 ⊢ -𝑒+∞ = if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞))
2		eqid 2734	. . 3 ⊢ +∞ = +∞
3	2	iftruei 4484	. 2 ⊢ if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) = -∞
4	1, 3	eqtri 2757	1 ⊢ -𝑒+∞ = -∞

Syntax hints:   = wceq 1541  ifcif 4477  +∞cpnf 11161  -∞cmnf 11162  -cneg 11363  -_𝑒cxne 13021

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 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-if 4478  df-xneg 13024

This theorem is referenced by:  xnegcl  13126  xnegneg  13127  xltnegi  13129  xnegid  13151  xnegdi  13161  xaddass2  13163  xsubge0  13174  xlesubadd  13176  xmulneg1  13182  xmulmnf1  13189  xadddi2  13210  xrsdsreclblem  21365  xblss2ps  24343  xblss2  24344  xaddeq0  32782  supminfxr  45650  liminflbuz2  46001