MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xnegpnf Unicode version

Theorem xnegpnf 10751
Description: Minus  +oo. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.)
Assertion
Ref Expression
xnegpnf  |-  - e  +oo  =  -oo

Proof of Theorem xnegpnf
StepHypRef Expression
1 df-xneg 10666 . 2  |-  - e  +oo  =  if (  +oo  =  +oo ,  -oo ,  if (  +oo  =  -oo , 
+oo ,  -u  +oo )
)
2 eqid 2404 . . 3  |-  +oo  =  +oo
3 iftrue 3705 . . 3  |-  (  +oo  =  +oo  ->  if (  +oo  =  +oo ,  -oo ,  if (  +oo  =  -oo ,  +oo ,  -u  +oo ) )  =  -oo )
42, 3ax-mp 8 . 2  |-  if ( 
+oo  =  +oo ,  -oo ,  if (  +oo  =  -oo ,  +oo ,  -u 
+oo ) )  = 
-oo
51, 4eqtri 2424 1  |-  - e  +oo  =  -oo
Colors of variables: wff set class
Syntax hints:    = wceq 1649   ifcif 3699    +oocpnf 9073    -oocmnf 9074   -ucneg 9248    - ecxne 10663
This theorem is referenced by:  xnegcl  10755  xnegneg  10756  xltnegi  10758  xnegid  10778  xnegdi  10783  xaddass2  10785  xsubge0  10796  xlesubadd  10798  xmulneg1  10804  xmulmnf1  10811  xadddi2  10832  xrsdsreclblem  16699  xblss2ps  18384  xblss2  18385  xaddeq0  24072
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-if 3700  df-xneg 10666
  Copyright terms: Public domain W3C validator