Theorem xnegpnf 12872

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 12777	. 2 ⊢ -𝑒+∞ = if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞))
2		eqid 2738	. . 3 ⊢ +∞ = +∞
3	2	iftruei 4463	. 2 ⊢ if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) = -∞
4	1, 3	eqtri 2766	1 ⊢ -𝑒+∞ = -∞

Syntax hints:   = wceq 1539  ifcif 4456  +∞cpnf 10937  -∞cmnf 10938  -cneg 11136  -_𝑒cxne 12774

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-if 4457  df-xneg 12777

This theorem is referenced by:  xnegcl  12876  xnegneg  12877  xltnegi  12879  xnegid  12901  xnegdi  12911  xaddass2  12913  xsubge0  12924  xlesubadd  12926  xmulneg1  12932  xmulmnf1  12939  xadddi2  12960  xrsdsreclblem  20556  xblss2ps  23462  xblss2  23463  xaddeq0  30978  supminfxr  42894  liminflbuz2  43246