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

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
StepHypRef Expression
1 df-xneg 12533 . 2 -𝑒+∞ = if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞))
2 eqid 2759 . . 3 +∞ = +∞
32iftruei 4420 . 2 if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) = -∞
41, 3eqtri 2782 1 -𝑒+∞ = -∞
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator