Theorem pnfnre 11122

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 11117	. . . 4 ⊢ +∞ = 𝒫 ∪ ℂ
2		pwuninel 8166	. . . 4 ⊢ ¬ 𝒫 ∪ ℂ ∈ ℂ
3	1, 2	eqneltri 2831	. . 3 ⊢ ¬ +∞ ∈ ℂ
4		recn 11067	. . 3 ⊢ (+∞ ∈ ℝ → +∞ ∈ ℂ)
5	3, 4	mto 196	. 2 ⊢ ¬ +∞ ∈ ℝ
6	5	nelir 3050	1 ⊢ +∞ ∉ ℝ

Syntax hints:   ∈ wcel 2106   ∉ wnel 3047  𝒫 cpw 4552  ∪ cuni 4857  ℂcc 10975  ℝcr 10976  +∞cpnf 11112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708  ax-sep 5248  ax-pr 5377  ax-un 7655  ax-resscn 11034

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-nel 3048  df-rab 3405  df-v 3444  df-un 3907  df-in 3909  df-ss 3919  df-pw 4554  df-sn 4579  df-pr 4581  df-uni 4858  df-pnf 11117

This theorem is referenced by:  pnfnre2  11123  renepnf  11129  ltxrlt  11151  nn0nepnf  12419  xrltnr  12961  pnfnlt  12970  xnn0lenn0nn0  13085  hashclb  14178  hasheq0  14183  pcgcd1  16676  pc2dvds  16678  ramtcl2  16810  odhash3  19278  xrsdsreclblem  20750  pnfnei  22477  iccpnfcnv  24213  i1f0rn  24952