Theorem pnfnre 10671

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 10666	. . . 4 ⊢ +∞ = 𝒫 ∪ ℂ
2		pwuninel 7924	. . . 4 ⊢ ¬ 𝒫 ∪ ℂ ∈ ℂ
3	1, 2	eqneltri 2883	. . 3 ⊢ ¬ +∞ ∈ ℂ
4		recn 10616	. . 3 ⊢ (+∞ ∈ ℝ → +∞ ∈ ℂ)
5	3, 4	mto 200	. 2 ⊢ ¬ +∞ ∈ ℝ
6	5	nelir 3094	1 ⊢ +∞ ∉ ℝ

Syntax hints:   ∈ wcel 2111   ∉ wnel 3091  𝒫 cpw 4497  ∪ cuni 4800  ℂcc 10524  ℝcr 10525  +∞cpnf 10661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295  ax-un 7441  ax-resscn 10583

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-nel 3092  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-pw 4499  df-sn 4526  df-pr 4528  df-uni 4801  df-pnf 10666

This theorem is referenced by:  pnfnre2  10672  renepnf  10678  ltxrlt  10700  nn0nepnf  11963  xrltnr  12502  pnfnlt  12511  xnn0lenn0nn0  12626  hashclb  13715  hasheq0  13720  pcgcd1  16203  pc2dvds  16205  ramtcl2  16337  odhash3  18693  xrsdsreclblem  20137  pnfnei  21825  iccpnfcnv  23549  i1f0rn  24286