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

Theorem xnegpnf 13233
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 13137 . 2 -𝑒+∞ = if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞))
2 eqid 2726 . . 3 +∞ = +∞
32iftruei 4530 . 2 if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) = -∞
41, 3eqtri 2754 1 -𝑒+∞ = -∞
Colors of variables: wff setvar class
Syntax hints:   = wceq 1534  ifcif 4523  +∞cpnf 11283  -∞cmnf 11284  -cneg 11483  -𝑒cxne 13134
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-if 4524  df-xneg 13137
This theorem is referenced by:  xnegcl  13237  xnegneg  13238  xltnegi  13240  xnegid  13262  xnegdi  13272  xaddass2  13274  xsubge0  13285  xlesubadd  13287  xmulneg1  13293  xmulmnf1  13300  xadddi2  13321  xrsdsreclblem  21402  xblss2ps  24392  xblss2  24393  xaddeq0  32657  supminfxr  45112  liminflbuz2  45469
  Copyright terms: Public domain W3C validator