Theorem xnegpnf 13145

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 13048	. 2 ⊢ -𝑒+∞ = if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞))
2		eqid 2729	. . 3 ⊢ +∞ = +∞
3	2	iftruei 4491	. 2 ⊢ if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) = -∞
4	1, 3	eqtri 2752	1 ⊢ -𝑒+∞ = -∞

Syntax hints:   = wceq 1540  ifcif 4484  +∞cpnf 11181  -∞cmnf 11182  -cneg 11382  -_𝑒cxne 13045

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4485  df-xneg 13048

This theorem is referenced by:  xnegcl  13149  xnegneg  13150  xltnegi  13152  xnegid  13174  xnegdi  13184  xaddass2  13186  xsubge0  13197  xlesubadd  13199  xmulneg1  13205  xmulmnf1  13212  xadddi2  13233  xrsdsreclblem  21354  xblss2ps  24322  xblss2  24323  xaddeq0  32726  supminfxr  45453  liminflbuz2  45806