Theorem xnegpnf 13235

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 13137	. 2 ⊢ -𝑒+∞ = if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞))
2		eqid 2769	. . 3 ⊢ +∞ = +∞
3	2	iftruei 4497	. 2 ⊢ if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) = -∞
4	1, 3	eqtri 2792	1 ⊢ -𝑒+∞ = -∞

Syntax hints:   = wceq 1567  ifcif 4490  +∞cpnf 11240  -∞cmnf 11241  -cneg 11442  -_𝑒cxne 13134

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-if 4491  df-xneg 13137

This theorem is referenced by:  xnegcl  13239  xnegneg  13240  xltnegi  13242  xnegid  13264  xnegdi  13274  xaddass2  13276  xsubge0  13287  xlesubadd  13289  xmulneg1  13295  xmulmnf1  13302  xadddi2  13323  xrsdsreclblem  21532  xblss2ps  24527  xblss2  24528  xaddeq0  33039  supminfxr  46105  liminflbuz2  46456