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

Theorem renepnf 9535
Description: No (finite) real equals plus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
Assertion
Ref Expression
renepnf  |-  ( A  e.  RR  ->  A  =/= +oo )

Proof of Theorem renepnf
StepHypRef Expression
1 pnfnre 9529 . . . 4  |- +oo  e/  RR
21neli 2783 . . 3  |-  -. +oo  e.  RR
3 eleq1 2523 . . 3  |-  ( A  = +oo  ->  ( A  e.  RR  <-> +oo  e.  RR ) )
42, 3mtbiri 303 . 2  |-  ( A  = +oo  ->  -.  A  e.  RR )
54necon2ai 2683 1  |-  ( A  e.  RR  ->  A  =/= +oo )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    e. wcel 1758    =/= wne 2644   RRcr 9385   +oocpnf 9519
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4514  ax-nul 4522  ax-pow 4571  ax-pr 4632  ax-un 6475  ax-resscn 9443
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-nel 2647  df-rex 2801  df-rab 2804  df-v 3073  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-nul 3739  df-pw 3963  df-sn 3979  df-pr 3981  df-uni 4193  df-pnf 9524
This theorem is referenced by:  renepnfd  9538  renfdisj  9541  xrnepnf  11204  rexneg  11285  rexadd  11306  xaddnepnf  11309  xaddcom  11312  xaddid1  11313  xnegdi  11315  xpncan  11318  xleadd1a  11320  rexmul  11338  xmulpnf1  11341  xadddilem  11361  rpsup  11815  hashneq0  12242  hash1snb  12282  euhash1  12283  xaddeq0  26190  ovoliunnfl  28574  voliunnfl  28576  volsupnfl  28577
  Copyright terms: Public domain W3C validator