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

Theorem xnegpnf 10531
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 10448 . 2  |-  - e  +oo  =  if (  +oo  =  +oo ,  -oo ,  if (  +oo  =  -oo , 
+oo ,  -u  +oo )
)
2 eqid 2285 . . 3  |-  +oo  =  +oo
3 iftrue 3573 . . 3  |-  (  +oo  =  +oo  ->  if (  +oo  =  +oo ,  -oo ,  if (  +oo  =  -oo ,  +oo ,  -u  +oo ) )  =  -oo )
42, 3ax-mp 10 . 2  |-  if ( 
+oo  =  +oo ,  -oo ,  if (  +oo  =  -oo ,  +oo ,  -u 
+oo ) )  = 
-oo
51, 4eqtri 2305 1  |-  - e  +oo  =  -oo
Colors of variables: wff set class
Syntax hints:    = wceq 1624   ifcif 3567    +oocpnf 8860    -oocmnf 8861   -ucneg 9034    - ecxne 10445
This theorem is referenced by:  xnegcl  10535  xnegneg  10536  xltnegi  10538  xnegid  10558  xnegdi  10563  xaddass2  10565  xsubge0  10576  xlesubadd  10578  xmulneg1  10584  xmulmnf1  10591  xadddi2  10612  xrsdsreclblem  16412  xblss2  17953
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-if 3568  df-xneg 10448
  Copyright terms: Public domain W3C validator