MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xnegpnf Structured version   Visualization version   GIF version

Theorem xnegpnf 11873
Description: Minus +∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.)
Assertion
Ref Expression
xnegpnf -𝑒+∞ = -∞

Proof of Theorem xnegpnf
StepHypRef Expression
1 df-xneg 11778 . 2 -𝑒+∞ = if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞))
2 eqid 2609 . . 3 +∞ = +∞
32iftruei 4042 . 2 if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) = -∞
41, 3eqtri 2631 1 -𝑒+∞ = -∞
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  ifcif 4035  +∞cpnf 9927  -∞cmnf 9928  -cneg 10118  -𝑒cxne 11775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-if 4036  df-xneg 11778
This theorem is referenced by:  xnegcl  11877  xnegneg  11878  xltnegi  11880  xnegid  11901  xnegdi  11907  xaddass2  11909  xsubge0  11920  xlesubadd  11922  xmulneg1  11928  xmulmnf1  11935  xadddi2  11956  xrsdsreclblem  19557  xblss2ps  21957  xblss2  21958  xaddeq0  28713
  Copyright terms: Public domain W3C validator