Theorem xnegpnf 13161

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 13063	. 2 ⊢ -𝑒+∞ = if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞))
2		eqid 2736	. . 3 ⊢ +∞ = +∞
3	2	iftruei 4473	. 2 ⊢ if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) = -∞
4	1, 3	eqtri 2759	1 ⊢ -𝑒+∞ = -∞

Syntax hints:   = wceq 1542  ifcif 4466  +∞cpnf 11176  -∞cmnf 11177  -cneg 11378  -_𝑒cxne 13060

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-if 4467  df-xneg 13063

This theorem is referenced by:  xnegcl  13165  xnegneg  13166  xltnegi  13168  xnegid  13190  xnegdi  13200  xaddass2  13202  xsubge0  13213  xlesubadd  13215  xmulneg1  13221  xmulmnf1  13228  xadddi2  13249  xrsdsreclblem  21393  xblss2ps  24366  xblss2  24367  xaddeq0  32826  supminfxr  45892  liminflbuz2  46243