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

Theorem xnegpnf 10536
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 10452 . 2  |-  - e  +oo  =  if (  +oo  =  +oo ,  -oo ,  if (  +oo  =  -oo , 
+oo ,  -u  +oo )
)
2 eqid 2283 . . 3  |-  +oo  =  +oo
3 iftrue 3571 . . 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 2303 1  |-  - e  +oo  =  -oo
Colors of variables: wff set class
Syntax hints:    = wceq 1623   ifcif 3565    +oocpnf 8864    -oocmnf 8865   -ucneg 9038    - ecxne 10449
This theorem is referenced by:  xnegcl  10540  xnegneg  10541  xltnegi  10543  xnegid  10563  xnegdi  10568  xaddass2  10570  xsubge0  10581  xlesubadd  10583  xmulneg1  10589  xmulmnf1  10596  xadddi2  10617  xrsdsreclblem  16417  xblss2  17958  xaddeq0  23304
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-if 3566  df-xneg 10452
  Copyright terms: Public domain W3C validator