Theorem pnfnre 11225

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 11220	. . . 4 ⊢ +∞ = 𝒫 ∪ ℂ
2		pwuninel 8257	. . . 4 ⊢ ¬ 𝒫 ∪ ℂ ∈ ℂ
3	1, 2	eqneltri 2883	. . 3 ⊢ ¬ +∞ ∈ ℂ
4		recn 11165	. . 3 ⊢ (+∞ ∈ ℝ → +∞ ∈ ℂ)
5	3, 4	mto 199	. 2 ⊢ ¬ +∞ ∈ ℝ
6	5	nelir 3066	1 ⊢ +∞ ∉ ℝ

Syntax hints:   ∈ wcel 2144   ∉ wnel 3063  𝒫 cpw 4557  ∪ cuni 4867  ℂcc 11073  ℝcr 11074  +∞cpnf 11215

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-sep 5248  ax-resscn 11132

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1101  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-nel 3064  df-rab 3417  df-v 3458  df-in 3913  df-ss 3923  df-pw 4559  df-uni 4868  df-pnf 11220

This theorem is referenced by:  pnfnre2  11226  renepnf  11232  ltxrlt  11255  nn0nepnf  12564  xrltnr  13123  pnfnlt  13132  xnn0lenn0nn0  13250  hashclb  14373  hasheq0  14378  pcgcd1  16915  pc2dvds  16917  ramtcl2  17049  odhash3  19618  xrsdsreclblem  21467  pnfnei  23282  iccpnfcnv  25008  i1f0rn  25746