Theorem pnfnre 11191

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 11186	. . . 4 ⊢ +∞ = 𝒫 ∪ ℂ
2		pwuninel 8231	. . . 4 ⊢ ¬ 𝒫 ∪ ℂ ∈ ℂ
3	1, 2	eqneltri 2847	. . 3 ⊢ ¬ +∞ ∈ ℂ
4		recn 11134	. . 3 ⊢ (+∞ ∈ ℝ → +∞ ∈ ℂ)
5	3, 4	mto 197	. 2 ⊢ ¬ +∞ ∈ ℝ
6	5	nelir 3032	1 ⊢ +∞ ∉ ℝ

Syntax hints:   ∈ wcel 2109   ∉ wnel 3029  𝒫 cpw 4559  ∪ cuni 4867  ℂcc 11042  ℝcr 11043  +∞cpnf 11181

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-pr 5382  ax-un 7691  ax-resscn 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nel 3030  df-rab 3403  df-v 3446  df-un 3916  df-in 3918  df-ss 3928  df-pw 4561  df-sn 4586  df-pr 4588  df-uni 4868  df-pnf 11186

This theorem is referenced by:  pnfnre2  11192  renepnf  11198  ltxrlt  11220  nn0nepnf  12499  xrltnr  13055  pnfnlt  13064  xnn0lenn0nn0  13181  hashclb  14299  hasheq0  14304  pcgcd1  16824  pc2dvds  16826  ramtcl2  16958  odhash3  19490  xrsdsreclblem  21354  pnfnei  23140  iccpnfcnv  24875  i1f0rn  25616