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

Theorem xnegpnf 12245
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 12151 . 2 -𝑒+∞ = if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞))
2 eqid 2771 . . 3 +∞ = +∞
32iftruei 4232 . 2 if(+∞ = +∞, -∞, if(+∞ = -∞, +∞, -+∞)) = -∞
41, 3eqtri 2793 1 -𝑒+∞ = -∞
Colors of variables: wff setvar class
Syntax hints:   = wceq 1631  ifcif 4225  +∞cpnf 10273  -∞cmnf 10274  -cneg 10469  -𝑒cxne 12148
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-if 4226  df-xneg 12151
This theorem is referenced by:  xnegcl  12249  xnegneg  12250  xltnegi  12252  xnegid  12274  xnegdi  12283  xaddass2  12285  xsubge0  12296  xlesubadd  12298  xmulneg1  12304  xmulmnf1  12311  xadddi2  12332  xrsdsreclblem  20007  xblss2ps  22426  xblss2  22427  xaddeq0  29858  supminfxr  40210
  Copyright terms: Public domain W3C validator