Theorem xnegpnf 13241

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

This proof depends on syntax axioms:   = wceq 1569  ifcif 4486  +∞cpnf 11246  -∞cmnf 11247  -cneg 11448  -_𝑒cxne 13140

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-if 4487  df-xneg 13143

This theorem is used by:  xnegcl  13245  xnegneg  13246  xltnegi  13248  xnegid  13270  xnegdi  13280  xaddass2  13282  xsubge0  13293  xlesubadd  13295  xmulneg1  13301  xmulmnf1  13308  xadddi2  13329  xrsdsreclblem  21574  xblss2ps  24569  xblss2  24570  xaddeq0  33109  supminfxr  46206  liminflbuz2  46557