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

Theorem pnfnre 10265
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 7562 . . . 4 ¬ 𝒫 ℂ ∈ ℂ
2 df-pnf 10260 . . . . 5 +∞ = 𝒫
32eleq1i 2822 . . . 4 (+∞ ∈ ℂ ↔ 𝒫 ℂ ∈ ℂ)
41, 3mtbir 312 . . 3 ¬ +∞ ∈ ℂ
5 recn 10210 . . 3 (+∞ ∈ ℝ → +∞ ∈ ℂ)
64, 5mto 188 . 2 ¬ +∞ ∈ ℝ
76nelir 3030 1 +∞ ∉ ℝ
Colors of variables: wff setvar class
Syntax hints:  wcel 2131  wnel 3027  𝒫 cpw 4294   cuni 4580  cc 10118  cr 10119  +∞cpnf 10255
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-sep 4925  ax-nul 4933  ax-pr 5047  ax-un 7106  ax-resscn 10177
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-nel 3028  df-rex 3048  df-rab 3051  df-v 3334  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-pw 4296  df-sn 4314  df-pr 4316  df-uni 4581  df-pnf 10260
This theorem is referenced by:  renepnf  10271  ltxrlt  10292  nn0nepnf  11555  xrltnr  12138  pnfnlt  12147  xnn0lenn0nn0  12260  hashclb  13333  hasheq0  13338  pcgcd1  15775  pc2dvds  15777  ramtcl2  15909  odhash3  18183  xrsdsreclblem  19986  pnfnei  21218  iccpnfcnv  22936  i1f0rn  23640  pnfnre2  40118
  Copyright terms: Public domain W3C validator