Theorem xnegpnf 13233

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 13137	. 2 ⊢ -𝑒+∞ = if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞))
2		eqid 2726	. . 3 ⊢ +∞ = +∞
3	2	iftruei 4530	. 2 ⊢ if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) = -∞
4	1, 3	eqtri 2754	1 ⊢ -𝑒+∞ = -∞

Syntax hints:   = wceq 1534  ifcif 4523  +∞cpnf 11283  -∞cmnf 11284  -cneg 11483  -_𝑒cxne 13134

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-if 4524  df-xneg 13137

This theorem is referenced by:  xnegcl  13237  xnegneg  13238  xltnegi  13240  xnegid  13262  xnegdi  13272  xaddass2  13274  xsubge0  13285  xlesubadd  13287  xmulneg1  13293  xmulmnf1  13300  xadddi2  13321  xrsdsreclblem  21402  xblss2ps  24392  xblss2  24393  xaddeq0  32657  supminfxr  45112  liminflbuz2  45469