Theorem xnegpnf 13156

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 13058	. 2 ⊢ -𝑒+∞ = if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞))
2		eqid 2741	. . 3 ⊢ +∞ = +∞
3	2	iftruei 4464	. 2 ⊢ if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) = -∞
4	1, 3	eqtri 2764	1 ⊢ -𝑒+∞ = -∞

Syntax hints:   = wceq 1548  ifcif 4457  +∞cpnf 11171  -∞cmnf 11172  -cneg 11373  -_𝑒cxne 13055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-if 4458  df-xneg 13058

This theorem is referenced by:  xnegcl  13160  xnegneg  13161  xltnegi  13163  xnegid  13185  xnegdi  13195  xaddass2  13197  xsubge0  13208  xlesubadd  13210  xmulneg1  13216  xmulmnf1  13223  xadddi2  13244  xrsdsreclblem  21392  xblss2ps  24388  xblss2  24389  xaddeq0  32849  supminfxr  45921  liminflbuz2  46272