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

Theorem xnegpnf 10502
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 10419 . 2  |-  - e  +oo  =  if (  +oo  =  +oo ,  -oo ,  if (  +oo  =  -oo , 
+oo ,  -u  +oo )
)
2 eqid 2258 . . 3  |-  +oo  =  +oo
3 iftrue 3545 . . 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 2278 1  |-  - e  +oo  =  -oo
Colors of variables: wff set class
Syntax hints:    = wceq 1619   ifcif 3539    +oocpnf 8832    -oocmnf 8833   -ucneg 9006    - ecxne 10416
This theorem is referenced by:  xnegcl  10506  xnegneg  10507  xltnegi  10509  xnegid  10529  xnegdi  10534  xaddass2  10536  xsubge0  10547  xlesubadd  10549  xmulneg1  10555  xmulmnf1  10562  xadddi2  10583  xrsdsreclblem  16379  xblss2  17920
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-if 3540  df-xneg 10419
  Copyright terms: Public domain W3C validator