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

Step	Hyp	Ref	Expression
1		df-pnf 11297	. . . 4 ⊢ +∞ = 𝒫 ∪ ℂ
2		pwuninel 8300	. . . 4 ⊢ ¬ 𝒫 ∪ ℂ ∈ ℂ
3	1, 2	eqneltri 2860	. . 3 ⊢ ¬ +∞ ∈ ℂ
4		recn 11245	. . 3 ⊢ (+∞ ∈ ℝ → +∞ ∈ ℂ)
5	3, 4	mto 197	. 2 ⊢ ¬ +∞ ∈ ℝ
6	5	nelir 3049	1 ⊢ +∞ ∉ ℝ

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