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

Theorem xnegmnf 12686
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 12590 . 2 -𝑒-∞ = if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞))
2 mnfnepnf 10775 . . 3 -∞ ≠ +∞
3 ifnefalse 4426 . . 3 (-∞ ≠ +∞ → if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞))
42, 3ax-mp 5 . 2 if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞)
5 eqid 2738 . . 3 -∞ = -∞
65iftruei 4421 . 2 if(-∞ = -∞, +∞, --∞) = +∞
71, 4, 63eqtri 2765 1 -𝑒-∞ = +∞
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  wne 2934  ifcif 4414  +∞cpnf 10750  -∞cmnf 10751  -cneg 10949  -𝑒cxne 12587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710  ax-sep 5167  ax-pow 5232  ax-un 7479  ax-cnex 10671
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-ne 2935  df-rab 3062  df-v 3400  df-un 3848  df-in 3850  df-ss 3860  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-uni 4797  df-pnf 10755  df-mnf 10756  df-xr 10757  df-xneg 12590
This theorem is referenced by:  xnegcl  12689  xnegneg  12690  xltnegi  12692  xnegid  12714  xnegdi  12724  xsubge0  12737  xmulneg1  12745  xmulpnf1n  12754  xadddi2  12773  xrsdsreclblem  20263  xaddeq0  30651  xrge0npcan  30880  carsgclctunlem2  31856  supminfxr  42544  supminfxr2  42549  liminf0  42876  liminflbuz2  42898  liminfpnfuz  42899
  Copyright terms: Public domain W3C validator