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

Theorem xnegmnf 12596
 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 12500 . 2 -𝑒-∞ = if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞))
2 mnfnepnf 10689 . . 3 -∞ ≠ +∞
3 ifnefalse 4481 . . 3 (-∞ ≠ +∞ → if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞))
42, 3ax-mp 5 . 2 if(-∞ = +∞, -∞, if(-∞ = -∞, +∞, --∞)) = if(-∞ = -∞, +∞, --∞)
5 eqid 2825 . . 3 -∞ = -∞
65iftruei 4476 . 2 if(-∞ = -∞, +∞, --∞) = +∞
71, 4, 63eqtri 2852 1 -𝑒-∞ = +∞
 Colors of variables: wff setvar class Syntax hints:   = wceq 1530   ≠ wne 3020  ifcif 4469  +∞cpnf 10664  -∞cmnf 10665  -cneg 10863  -𝑒cxne 12497 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-sep 5199  ax-pow 5262  ax-un 7454  ax-cnex 10585 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-rex 3148  df-rab 3151  df-v 3501  df-un 3944  df-in 3946  df-ss 3955  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-uni 4837  df-pnf 10669  df-mnf 10670  df-xr 10671  df-xneg 12500 This theorem is referenced by:  xnegcl  12599  xnegneg  12600  xltnegi  12602  xnegid  12624  xnegdi  12634  xsubge0  12647  xmulneg1  12655  xmulpnf1n  12664  xadddi2  12683  xrsdsreclblem  20509  xaddeq0  30392  xrge0npcan  30597  carsgclctunlem2  31465  supminfxr  41607  supminfxr2  41612  liminf0  41941  liminflbuz2  41963  liminfpnfuz  41964
 Copyright terms: Public domain W3C validator