Theorem xnegpnf 12628

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 12533	. 2 ⊢ -𝑒+∞ = if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞))
2		eqid 2759	. . 3 ⊢ +∞ = +∞
3	2	iftruei 4420	. 2 ⊢ if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) = -∞
4	1, 3	eqtri 2782	1 ⊢ -𝑒+∞ = -∞

Syntax hints:   = wceq 1539  ifcif 4413  +∞cpnf 10695  -∞cmnf 10696  -cneg 10894  -_𝑒cxne 12530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-if 4414  df-xneg 12533

This theorem is referenced by:  xnegcl  12632  xnegneg  12633  xltnegi  12635  xnegid  12657  xnegdi  12667  xaddass2  12669  xsubge0  12680  xlesubadd  12682  xmulneg1  12688  xmulmnf1  12695  xadddi2  12716  xrsdsreclblem  20197  xblss2ps  23088  xblss2  23089  xaddeq0  30585  supminfxr  42454  liminflbuz2  42808