Theorem xnegpnf 13308

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 13210	. 2 ⊢ -𝑒+∞ = if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞))
2		eqid 2760	. . 3 ⊢ +∞ = +∞
3	2	iftruei 4488	. 2 ⊢ if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) = -∞
4	1, 3	eqtri 2783	1 ⊢ -𝑒+∞ = -∞

This proof depends on syntax axioms:   = wceq 1570  ifcif 4481  +∞cpnf 11311  -∞cmnf 11312  -cneg 11513  -_𝑒cxne 13207

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-if 4482  df-xneg 13210

This theorem is used by:  xnegcl  13312  xnegneg  13313  xltnegi  13315  xnegid  13337  xnegdi  13347  xaddass2  13349  xsubge0  13360  xlesubadd  13362  xmulneg1  13368  xmulmnf1  13375  xadddi2  13396  xrsdsreclblem  21680  xblss2ps  24681  xblss2  24682  xaddeq0  33278  supminfxr  46396  liminflbuz2  46747