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

Theorem pnfnre 10398
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 7666 . . . 4 ¬ 𝒫 ℂ ∈ ℂ
2 df-pnf 10393 . . . . 5 +∞ = 𝒫
32eleq1i 2897 . . . 4 (+∞ ∈ ℂ ↔ 𝒫 ℂ ∈ ℂ)
41, 3mtbir 315 . . 3 ¬ +∞ ∈ ℂ
5 recn 10342 . . 3 (+∞ ∈ ℝ → +∞ ∈ ℂ)
64, 5mto 189 . 2 ¬ +∞ ∈ ℝ
76nelir 3105 1 +∞ ∉ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2166  wnel 3102  𝒫 cpw 4378   cuni 4658  cc 10250  cr 10251  +∞cpnf 10388
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pr 5127  ax-un 7209  ax-resscn 10309
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-nel 3103  df-rex 3123  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-pw 4380  df-sn 4398  df-pr 4400  df-uni 4659  df-pnf 10393
This theorem is referenced by:  renepnf  10404  ltxrlt  10427  nn0nepnf  11698  xrltnr  12239  pnfnlt  12248  xnn0lenn0nn0  12363  hashclb  13439  hasheq0  13444  pcgcd1  15952  pc2dvds  15954  ramtcl2  16086  odhash3  18342  xrsdsreclblem  20152  pnfnei  21395  iccpnfcnv  23113  i1f0rn  23848  pnfnre2  40423
  Copyright terms: Public domain W3C validator