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

Theorem xnegmnf 12591
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 12495 . 2 -𝑒-∞ = if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞))
2 mnfnepnf 10685 . . 3 -∞ ≠ +∞
3 ifnefalse 4475 . . 3 (-∞ ≠ +∞ → if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞))
42, 3ax-mp 5 . 2 if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞)
5 eqid 2818 . . 3 -∞ = -∞
65iftruei 4470 . 2 if(-∞ = -∞, +∞, --∞) = +∞
71, 4, 63eqtri 2845 1 -𝑒-∞ = +∞
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  wne 3013  ifcif 4463  +∞cpnf 10660  -∞cmnf 10661  -cneg 10859  -𝑒cxne 12492
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-pow 5257  ax-un 7450  ax-cnex 10581
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-rex 3141  df-rab 3144  df-v 3494  df-un 3938  df-in 3940  df-ss 3949  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-uni 4831  df-pnf 10665  df-mnf 10666  df-xr 10667  df-xneg 12495
This theorem is referenced by:  xnegcl  12594  xnegneg  12595  xltnegi  12597  xnegid  12619  xnegdi  12629  xsubge0  12642  xmulneg1  12650  xmulpnf1n  12659  xadddi2  12678  xrsdsreclblem  20519  xaddeq0  30403  xrge0npcan  30608  carsgclctunlem2  31476  supminfxr  41616  supminfxr2  41621  liminf0  41950  liminflbuz2  41972  liminfpnfuz  41973
  Copyright terms: Public domain W3C validator