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

Theorem xnegpnf 12597
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 12502 . 2 -𝑒+∞ = if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞))
2 eqid 2826 . . 3 +∞ = +∞
32iftruei 4477 . 2 if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) = -∞
41, 3eqtri 2849 1 -𝑒+∞ = -∞
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  ifcif 4470  +∞cpnf 10666  -∞cmnf 10667  -cneg 10865  -𝑒cxne 12499
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-ex 1774  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-if 4471  df-xneg 12502
This theorem is referenced by:  xnegcl  12601  xnegneg  12602  xltnegi  12604  xnegid  12626  xnegdi  12636  xaddass2  12638  xsubge0  12649  xlesubadd  12651  xmulneg1  12657  xmulmnf1  12664  xadddi2  12685  xrsdsreclblem  20526  xblss2ps  22945  xblss2  22946  xaddeq0  30409  supminfxr  41624  liminflbuz2  41980
  Copyright terms: Public domain W3C validator