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

Theorem pnfnre 11302
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 df-pnf 11297 . . . 4 +∞ = 𝒫
2 pwuninel 8300 . . . 4 ¬ 𝒫 ℂ ∈ ℂ
31, 2eqneltri 2860 . . 3 ¬ +∞ ∈ ℂ
4 recn 11245 . . 3 (+∞ ∈ ℝ → +∞ ∈ ℂ)
53, 4mto 197 . 2 ¬ +∞ ∈ ℝ
65nelir 3049 1 +∞ ∉ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2108  wnel 3046  𝒫 cpw 4600   cuni 4907  cc 11153  cr 11154  +∞cpnf 11292
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-pr 5432  ax-un 7755  ax-resscn 11212
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nel 3047  df-rab 3437  df-v 3482  df-un 3956  df-in 3958  df-ss 3968  df-pw 4602  df-sn 4627  df-pr 4629  df-uni 4908  df-pnf 11297
This theorem is referenced by:  pnfnre2  11303  renepnf  11309  ltxrlt  11331  nn0nepnf  12607  xrltnr  13161  pnfnlt  13170  xnn0lenn0nn0  13287  hashclb  14397  hasheq0  14402  pcgcd1  16915  pc2dvds  16917  ramtcl2  17049  odhash3  19594  xrsdsreclblem  21430  pnfnei  23228  iccpnfcnv  24975  i1f0rn  25717
  Copyright terms: Public domain W3C validator