Theorem pnfnre 11277

Description: Plus infinity is not a real number. (Contributed by NM, 13-Oct-2005.)

Assertion

Ref	Expression
pnfnre	⊢ +∞ ∉ ℝ

Proof of Theorem pnfnre

Step	Hyp	Ref	Expression
1		df-pnf 11272	. . . 4 ⊢ +∞ = 𝒫 ∪ ℂ
2		pwuninel 8276	. . . 4 ⊢ ¬ 𝒫 ∪ ℂ ∈ ℂ
3	1, 2	eqneltri 2881	. . 3 ⊢ ¬ +∞ ∈ ℂ
4		recn 11217	. . 3 ⊢ (+∞ ∈ ℝ → +∞ ∈ ℂ)
5	3, 4	mto 200	. 2 ⊢ ¬ +∞ ∈ ℝ
6	5	nelir 3066	1 ⊢ +∞ ∉ ℝ

This proof depends on syntax axioms:   ∈ wcel 2145   ∉ wnel 3063  𝒫 cpw 4560  ∪ cuni 4870  ℂcc 11125  ℝcr 11126  +∞cpnf 11267

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-resscn 11184

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-nel 3064  df-rab 3415  df-v 3455  df-in 3909  df-ss 3919  df-pw 4562  df-uni 4871  df-pnf 11272

This theorem is used by:  pnfnre2  11278  renepnf  11284  ltxrlt  11307  nn0nepnf  12612  xrltnr  13172  pnfnlt  13181  xnn0lenn0nn0  13299  hashclb  14424  hasheq0  14429  pcgcd1  16973  pc2dvds  16975  ramtcl2  17107  odhash3  19704  xrsdsreclblem  21627  pnfnei  23446  iccpnfcnv  25173  i1f0rn  25911