Theorem xnegpnf 13271

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 13175	. 2 ⊢ -𝑒+∞ = if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞))
2		eqid 2740	. . 3 ⊢ +∞ = +∞
3	2	iftruei 4555	. 2 ⊢ if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) = -∞
4	1, 3	eqtri 2768	1 ⊢ -𝑒+∞ = -∞

Syntax hints:   = wceq 1537  ifcif 4548  +∞cpnf 11321  -∞cmnf 11322  -cneg 11521  -_𝑒cxne 13172

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-if 4549  df-xneg 13175

This theorem is referenced by:  xnegcl  13275  xnegneg  13276  xltnegi  13278  xnegid  13300  xnegdi  13310  xaddass2  13312  xsubge0  13323  xlesubadd  13325  xmulneg1  13331  xmulmnf1  13338  xadddi2  13359  xrsdsreclblem  21453  xblss2ps  24432  xblss2  24433  xaddeq0  32760  supminfxr  45379  liminflbuz2  45736