Theorem xnegpnf 13111

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 13014	. 2 ⊢ -𝑒+∞ = if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞))
2		eqid 2729	. . 3 ⊢ +∞ = +∞
3	2	iftruei 4483	. 2 ⊢ if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) = -∞
4	1, 3	eqtri 2752	1 ⊢ -𝑒+∞ = -∞

Syntax hints:   = wceq 1540  ifcif 4476  +∞cpnf 11146  -∞cmnf 11147  -cneg 11348  -_𝑒cxne 13011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4477  df-xneg 13014

This theorem is referenced by:  xnegcl  13115  xnegneg  13116  xltnegi  13118  xnegid  13140  xnegdi  13150  xaddass2  13152  xsubge0  13163  xlesubadd  13165  xmulneg1  13171  xmulmnf1  13178  xadddi2  13199  xrsdsreclblem  21319  xblss2ps  24287  xblss2  24288  xaddeq0  32697  supminfxr  45453  liminflbuz2  45806