Theorem pnfnre 11307

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 11302	. . . 4 ⊢ +∞ = 𝒫 ∪ ℂ
2		pwuninel 8271	. . . 4 ⊢ ¬ 𝒫 ∪ ℂ ∈ ℂ
3	1, 2	eqneltri 2879	. . 3 ⊢ ¬ +∞ ∈ ℂ
4		recn 11247	. . 3 ⊢ (+∞ ∈ ℝ → +∞ ∈ ℂ)
5	3, 4	mto 200	. 2 ⊢ ¬ +∞ ∈ ℝ
6	5	nelir 3064	1 ⊢ +∞ ∉ ℝ

This proof depends on syntax axioms:   ∈ wcel 2145   ∉ wnel 3061  𝒫 cpw 4557  ∪ cuni 4867  ℂcc 11155  ℝcr 11156  +∞cpnf 11297

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5249  ax-resscn 11214

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-nel 3062  df-rab 3413  df-v 3452  df-in 3906  df-ss 3916  df-pw 4559  df-uni 4868  df-pnf 11302

This theorem is used by:  pnfnre2  11308  renepnf  11314  ltxrlt  11337  nn0nepnf  12642  xrltnr  13203  pnfnlt  13212  xnn0lenn0nn0  13330  hashclb  14455  hasheq0  14460  pcgcd1  17002  pc2dvds  17004  ramtcl2  17136  odhash3  19737  xrsdsreclblem  21666  pnfnei  23485  iccpnfcnv  25212  i1f0rn  25950