Theorem xnegpnf 13263

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

This proof depends on syntax axioms:   = wceq 1570  ifcif 4485  +∞cpnf 11267  -∞cmnf 11268  -cneg 11469  -_𝑒cxne 13162

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-if 4486  df-xneg 13165

This theorem is used by:  xnegcl  13267  xnegneg  13268  xltnegi  13270  xnegid  13292  xnegdi  13302  xaddass2  13304  xsubge0  13315  xlesubadd  13317  xmulneg1  13323  xmulmnf1  13330  xadddi2  13351  xrsdsreclblem  21627  xblss2ps  24628  xblss2  24629  xaddeq0  33211  supminfxr  46279  liminflbuz2  46630