Theorem xnegpnf 13169

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

Syntax hints:   = wceq 1540  ifcif 4488  +∞cpnf 11205  -∞cmnf 11206  -cneg 11406  -_𝑒cxne 13069

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 4489  df-xneg 13072

This theorem is referenced by:  xnegcl  13173  xnegneg  13174  xltnegi  13176  xnegid  13198  xnegdi  13208  xaddass2  13210  xsubge0  13221  xlesubadd  13223  xmulneg1  13229  xmulmnf1  13236  xadddi2  13257  xrsdsreclblem  21329  xblss2ps  24289  xblss2  24290  xaddeq0  32676  supminfxr  45460  liminflbuz2  45813