Theorem pnfnre 11016

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 11011	. . . 4 ⊢ +∞ = 𝒫 ∪ ℂ
2		pwuninel 8091	. . . 4 ⊢ ¬ 𝒫 ∪ ℂ ∈ ℂ
3	1, 2	eqneltri 2832	. . 3 ⊢ ¬ +∞ ∈ ℂ
4		recn 10961	. . 3 ⊢ (+∞ ∈ ℝ → +∞ ∈ ℂ)
5	3, 4	mto 196	. 2 ⊢ ¬ +∞ ∈ ℝ
6	5	nelir 3052	1 ⊢ +∞ ∉ ℝ

Syntax hints:   ∈ wcel 2106   ∉ wnel 3049  𝒫 cpw 4533  ∪ cuni 4839  ℂcc 10869  ℝcr 10870  +∞cpnf 11006

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7588  ax-resscn 10928

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-nel 3050  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-pw 4535  df-sn 4562  df-pr 4564  df-uni 4840  df-pnf 11011

This theorem is referenced by:  pnfnre2  11017  renepnf  11023  ltxrlt  11045  nn0nepnf  12313  xrltnr  12855  pnfnlt  12864  xnn0lenn0nn0  12979  hashclb  14073  hasheq0  14078  pcgcd1  16578  pc2dvds  16580  ramtcl2  16712  odhash3  19181  xrsdsreclblem  20644  pnfnei  22371  iccpnfcnv  24107  i1f0rn  24846