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

Theorem xnegpnf 12590
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 12495 . 2 -𝑒+∞ = if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞))
2 eqid 2818 . . 3 +∞ = +∞
32iftruei 4470 . 2 if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) = -∞
41, 3eqtri 2841 1 -𝑒+∞ = -∞
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  ifcif 4463  +∞cpnf 10660  -∞cmnf 10661  -cneg 10859  -𝑒cxne 12492
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-ex 1772  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-if 4464  df-xneg 12495
This theorem is referenced by:  xnegcl  12594  xnegneg  12595  xltnegi  12597  xnegid  12619  xnegdi  12629  xaddass2  12631  xsubge0  12642  xlesubadd  12644  xmulneg1  12650  xmulmnf1  12657  xadddi2  12678  xrsdsreclblem  20519  xblss2ps  22938  xblss2  22939  xaddeq0  30403  supminfxr  41616  liminflbuz2  41972
  Copyright terms: Public domain W3C validator