Theorem xnegpnf 12590

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 12495	. 2 ⊢ -𝑒+∞ = if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞))
2		eqid 2798	. . 3 ⊢ +∞ = +∞
3	2	iftruei 4432	. 2 ⊢ if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) = -∞
4	1, 3	eqtri 2821	1 ⊢ -𝑒+∞ = -∞

Syntax hints:   = wceq 1538  ifcif 4425  +∞cpnf 10661  -∞cmnf 10662  -cneg 10860  -_𝑒cxne 12492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-if 4426  df-xneg 12495

This theorem is referenced by:  xnegcl  12594  xnegneg  12595  xltnegi  12597  xnegid  12619  xnegdi  12629  xaddass2  12631  xsubge0  12642  xlesubadd  12644  xmulneg1  12650  xmulmnf1  12657  xadddi2  12678  xrsdsreclblem  20137  xblss2ps  23008  xblss2  23009  xaddeq0  30503  supminfxr  42103  liminflbuz2  42457