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

Theorem pnfnre 9562
Description: Plus infinity is not a real number. (Contributed by NM, 13-Oct-2005.)
Assertion
Ref Expression
pnfnre

Proof of Theorem pnfnre
StepHypRef Expression
1 pwuninel 6928 . . . 4
2 df-pnf 9557 . . . . 5
32eleq1i 2531 . . . 4
41, 3mtbir 299 . . 3
5 recn 9509 . . 3
64, 5mto 176 . 2
76nelir 2789 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1758  e/wnel 2649  ~Pcpw 3976  U.cuni 4208   cc 9417   cr 9418   cpnf 9552
This theorem is referenced by:  renepnf  9568  ltxrlt  9582  xrltnr  11240  pnfnlt  11247  hashclb  12285  hasheq0  12288  pcgcd1  14101  pc2dvds  14103  ramtcl2  14230  odhash3  16236  xrsdsreclblem  18052  pnfnei  19223  iccpnfcnv  20915  i1f0rn  21560
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 1955  ax-ext 2432  ax-sep 4530  ax-nul 4538  ax-pow 4587  ax-pr 4648  ax-un 6505  ax-resscn 9476
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 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-nel 2651  df-rex 2806  df-rab 2809  df-v 3083  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3752  df-pw 3978  df-sn 3994  df-pr 3996  df-uni 4209  df-pnf 9557
  Copyright terms: Public domain W3C validator