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

Theorem xnegmnf 12038
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 11943 . 2 -𝑒-∞ = if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞))
2 mnfnepnf 10092 . . 3 -∞ ≠ +∞
3 ifnefalse 4096 . . 3 (-∞ ≠ +∞ → if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞))
42, 3ax-mp 5 . 2 if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞)
5 eqid 2621 . . 3 -∞ = -∞
65iftruei 4091 . 2 if(-∞ = -∞, +∞, --∞) = +∞
71, 4, 63eqtri 2647 1 -𝑒-∞ = +∞
Colors of variables: wff setvar class
Syntax hints:   = wceq 1482  wne 2793  ifcif 4084  +∞cpnf 10068  -∞cmnf 10069  -cneg 10264  -𝑒cxne 11940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-sep 4779  ax-pow 4841  ax-un 6946  ax-cnex 9989
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-nel 2897  df-rex 2917  df-rab 2920  df-v 3200  df-un 3577  df-in 3579  df-ss 3586  df-if 4085  df-pw 4158  df-sn 4176  df-pr 4178  df-uni 4435  df-pnf 10073  df-mnf 10074  df-xr 10075  df-xneg 11943
This theorem is referenced by:  xnegcl  12041  xnegneg  12042  xltnegi  12044  xnegid  12066  xnegdi  12075  xsubge0  12088  xmulneg1  12096  xmulpnf1n  12105  xadddi2  12124  xrsdsreclblem  19786  xaddeq0  29503  xrge0npcan  29679  carsgclctunlem2  30366  supminfxr  39513  supminfxr2  39518  liminf0  39825
  Copyright terms: Public domain W3C validator