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

Theorem xnegmnf 11870
Description: Minus -∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) (Revised by Mario Carneiro, 20-Aug-2015.)
Assertion
Ref Expression
xnegmnf -𝑒-∞ = +∞

Proof of Theorem xnegmnf
StepHypRef Expression
1 df-xneg 11774 . 2 -𝑒-∞ = if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞))
2 mnfnepnf 11783 . . 3 -∞ ≠ +∞
3 ifnefalse 4043 . . 3 (-∞ ≠ +∞ → if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞))
42, 3ax-mp 5 . 2 if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞)
5 eqid 2605 . . 3 -∞ = -∞
65iftruei 4038 . 2 if(-∞ = -∞, +∞, --∞) = +∞
71, 4, 63eqtri 2631 1 -𝑒-∞ = +∞
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  wne 2775  ifcif 4031  +∞cpnf 9923  -∞cmnf 9924  -cneg 10114  -𝑒cxne 11771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-sep 4699  ax-pow 4760  ax-un 6820  ax-cnex 9844
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ne 2777  df-nel 2778  df-rex 2897  df-rab 2900  df-v 3170  df-un 3540  df-in 3542  df-ss 3549  df-if 4032  df-pw 4105  df-sn 4121  df-pr 4123  df-uni 4363  df-pnf 9928  df-mnf 9929  df-xr 9930  df-xneg 11774
This theorem is referenced by:  xnegcl  11873  xnegneg  11874  xltnegi  11876  xnegid  11897  xnegdi  11903  xsubge0  11916  xmulneg1  11924  xmulpnf1n  11933  xadddi2  11952  xrsdsreclblem  19553  xaddeq0  28709  xrge0npcan  28827  carsgclctunlem2  29510
  Copyright terms: Public domain W3C validator