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

Theorem xnegmnf 12944
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 12848 . 2 -𝑒-∞ = if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞))
2 mnfnepnf 11031 . . 3 -∞ ≠ +∞
3 ifnefalse 4471 . . 3 (-∞ ≠ +∞ → if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞))
42, 3ax-mp 5 . 2 if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞)
5 eqid 2738 . . 3 -∞ = -∞
65iftruei 4466 . 2 if(-∞ = -∞, +∞, --∞) = +∞
71, 4, 63eqtri 2770 1 -𝑒-∞ = +∞
Colors of variables: wff setvar class
Syntax hints:   = wceq 1539  wne 2943  ifcif 4459  +∞cpnf 11006  -∞cmnf 11007  -cneg 11206  -𝑒cxne 12845
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-pow 5288  ax-un 7588  ax-cnex 10927
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-rab 3073  df-v 3434  df-un 3892  df-in 3894  df-ss 3904  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-uni 4840  df-pnf 11011  df-mnf 11012  df-xr 11013  df-xneg 12848
This theorem is referenced by:  xnegcl  12947  xnegneg  12948  xltnegi  12950  xnegid  12972  xnegdi  12982  xsubge0  12995  xmulneg1  13003  xmulpnf1n  13012  xadddi2  13031  xrsdsreclblem  20644  xaddeq0  31076  xrge0npcan  31303  carsgclctunlem2  32286  supminfxr  43004  supminfxr2  43009  liminf0  43334  liminflbuz2  43356  liminfpnfuz  43357
  Copyright terms: Public domain W3C validator