Theorem xnegpnf 13192

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 13096	. 2 ⊢ -𝑒+∞ = if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞))
2		eqid 2730	. . 3 ⊢ +∞ = +∞
3	2	iftruei 4534	. 2 ⊢ if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) = -∞
4	1, 3	eqtri 2758	1 ⊢ -𝑒+∞ = -∞

Syntax hints:   = wceq 1539  ifcif 4527  +∞cpnf 11249  -∞cmnf 11250  -cneg 11449  -_𝑒cxne 13093

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-if 4528  df-xneg 13096

This theorem is referenced by:  xnegcl  13196  xnegneg  13197  xltnegi  13199  xnegid  13221  xnegdi  13231  xaddass2  13233  xsubge0  13244  xlesubadd  13246  xmulneg1  13252  xmulmnf1  13259  xadddi2  13280  xrsdsreclblem  21191  xblss2ps  24127  xblss2  24128  xaddeq0  32233  supminfxr  44472  liminflbuz2  44829