Theorem pnfnre 11215

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

Syntax hints:   ∈ wcel 2109   ∉ wnel 3029  𝒫 cpw 4563  ∪ cuni 4871  ℂcc 11066  ℝcr 11067  +∞cpnf 11205

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 5251  ax-pr 5387  ax-un 7711  ax-resscn 11125

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 3406  df-v 3449  df-un 3919  df-in 3921  df-ss 3931  df-pw 4565  df-sn 4590  df-pr 4592  df-uni 4872  df-pnf 11210

This theorem is referenced by:  pnfnre2  11216  renepnf  11222  ltxrlt  11244  nn0nepnf  12523  xrltnr  13079  pnfnlt  13088  xnn0lenn0nn0  13205  hashclb  14323  hasheq0  14328  pcgcd1  16848  pc2dvds  16850  ramtcl2  16982  odhash3  19506  xrsdsreclblem  21329  pnfnei  23107  iccpnfcnv  24842  i1f0rn  25583