Theorem pnfnre 11350

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

This proof depends on syntax axioms:   ∈ wcel 2144   ∉ wnel 3061  𝒫 cpw 4556  ∪ cuni 4866  ℂcc 11198  ℝcr 11199  +∞cpnf 11340

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-resscn 11257

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nel 3062  df-rab 3413  df-v 3452  df-ss 3896  df-in 4091  df-pw 4558  df-uni 4867  df-pnf 11345

This theorem is used by:  pnfnre2  11351  renepnf  11357  ltxrlt  11380  nn0nepnf  12687  xrltnr  13248  pnfnlt  13257  xnn0lenn0nn0  13375  hashclb  14502  hasheq0  14507  pcgcd1  17055  pc2dvds  17057  ramtcl2  17189  odhash3  19790  xrsdsreclblem  21719  pnfnei  23538  iccpnfcnv  25265  i1f0rn  26003