Theorem xnegpnf 13124

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

Syntax hints:   = wceq 1541  ifcif 4479  +∞cpnf 11163  -∞cmnf 11164  -cneg 11365  -_𝑒cxne 13023

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-if 4480  df-xneg 13026

This theorem is referenced by:  xnegcl  13128  xnegneg  13129  xltnegi  13131  xnegid  13153  xnegdi  13163  xaddass2  13165  xsubge0  13176  xlesubadd  13178  xmulneg1  13184  xmulmnf1  13191  xadddi2  13212  xrsdsreclblem  21367  xblss2ps  24345  xblss2  24346  xaddeq0  32833  supminfxr  45708  liminflbuz2  46059