Theorem xnegpnf 13126

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 13028	. 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 11165  -∞cmnf 11166  -cneg 11367  -_𝑒cxne 13025

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 13028

This theorem is referenced by:  xnegcl  13130  xnegneg  13131  xltnegi  13133  xnegid  13155  xnegdi  13165  xaddass2  13167  xsubge0  13178  xlesubadd  13180  xmulneg1  13186  xmulmnf1  13193  xadddi2  13214  xrsdsreclblem  21369  xblss2ps  24347  xblss2  24348  xaddeq0  32835  supminfxr  45729  liminflbuz2  46080