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

Theorem renepnf 9690
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 9684 . . . 4  |- +oo  e/  RR
21neli 2761 . . 3  |-  -. +oo  e.  RR
3 eleq1 2495 . . 3  |-  ( A  = +oo  ->  ( A  e.  RR  <-> +oo  e.  RR ) )
42, 3mtbiri 305 . 2  |-  ( A  = +oo  ->  -.  A  e.  RR )
54necon2ai 2660 1  |-  ( A  e.  RR  ->  A  =/= +oo )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1438    e. wcel 1869    =/= wne 2619   RRcr 9540   +oocpnf 9674
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pow 4600  ax-pr 4658  ax-un 6595  ax-resscn 9598
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-nel 2622  df-rex 2782  df-rab 2785  df-v 3084  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-pw 3982  df-sn 3998  df-pr 4000  df-uni 4218  df-pnf 9679
This theorem is referenced by:  renepnfd  9693  renfdisj  9696  xrnepnf  11422  rexneg  11506  rexadd  11527  xaddnepnf  11530  xaddcom  11533  xaddid1  11534  xnegdi  11536  xpncan  11539  xleadd1a  11541  rexmul  11559  xmulpnf1  11562  xadddilem  11582  rpsup  12094  hashneq0  12546  hash1snb  12592  xrsnsgrp  18997  xaddeq0  28330  icorempt2  31712  ovoliunnfl  31940  voliunnfl  31942  volsupnfl  31943  supxrgelem  37446  supxrge  37447  sge0repnf  38060
  Copyright terms: Public domain W3C validator