Theorem xnegpnf 13234

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 13136	. 2 ⊢ -𝑒+∞ = if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞))
2		eqid 2761	. . 3 ⊢ +∞ = +∞
3	2	iftruei 4493	. 2 ⊢ if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) = -∞
4	1, 3	eqtri 2784	1 ⊢ -𝑒+∞ = -∞

Syntax hints:   = wceq 1568  ifcif 4486  +∞cpnf 11239  -∞cmnf 11240  -cneg 11441  -_𝑒cxne 13133

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-if 4487  df-xneg 13136

This theorem is referenced by:  xnegcl  13238  xnegneg  13239  xltnegi  13241  xnegid  13263  xnegdi  13273  xaddass2  13275  xsubge0  13286  xlesubadd  13288  xmulneg1  13294  xmulmnf1  13301  xadddi2  13322  xrsdsreclblem  21542  xblss2ps  24537  xblss2  24538  xaddeq0  33064  supminfxr  46126  liminflbuz2  46477