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

Theorem pnfnre 9628
Description: Plus infinity is not a real number. (Contributed by NM, 13-Oct-2005.)
Assertion
Ref Expression
pnfnre  |- +oo  e/  RR

Proof of Theorem pnfnre
StepHypRef Expression
1 pwuninel 6972 . . . 4  |-  -.  ~P U. CC  e.  CC
2 df-pnf 9623 . . . . 5  |- +oo  =  ~P U. CC
32eleq1i 2492 . . . 4  |-  ( +oo  e.  CC  <->  ~P U. CC  e.  CC )
41, 3mtbir 300 . . 3  |-  -. +oo  e.  CC
5 recn 9575 . . 3  |-  ( +oo  e.  RR  -> +oo  e.  CC )
64, 5mto 179 . 2  |-  -. +oo  e.  RR
76nelir 2699 1  |- +oo  e/  RR
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1872    e/ wnel 2595   ~Pcpw 3919   U.cuni 4157   CCcc 9483   RRcr 9484   +oocpnf 9618
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536  ax-resscn 9542
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-nel 2597  df-rex 2715  df-rab 2718  df-v 3019  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-pw 3921  df-sn 3937  df-pr 3939  df-uni 4158  df-pnf 9623
This theorem is referenced by:  renepnf  9634  ltxrlt  9650  xrltnr  11367  pnfnlt  11376  hashclb  12485  hasheq0  12489  pcgcd1  14764  pc2dvds  14766  ramtcl2  14904  ramtcl2OLD  14905  odhash3  17163  xrsdsreclblem  18952  pnfnei  20173  iccpnfcnv  21909  i1f0rn  22577
  Copyright terms: Public domain W3C validator