Theorem pnfnre 11171

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 11166	. . . 4 ⊢ +∞ = 𝒫 ∪ ℂ
2		pwuninel 8215	. . . 4 ⊢ ¬ 𝒫 ∪ ℂ ∈ ℂ
3	1, 2	eqneltri 2853	. . 3 ⊢ ¬ +∞ ∈ ℂ
4		recn 11114	. . 3 ⊢ (+∞ ∈ ℝ → +∞ ∈ ℂ)
5	3, 4	mto 197	. 2 ⊢ ¬ +∞ ∈ ℝ
6	5	nelir 3037	1 ⊢ +∞ ∉ ℝ

Syntax hints:   ∈ wcel 2113   ∉ wnel 3034  𝒫 cpw 4552  ∪ cuni 4861  ℂcc 11022  ℝcr 11023  +∞cpnf 11161

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-pr 5375  ax-un 7678  ax-resscn 11081

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-nel 3035  df-rab 3398  df-v 3440  df-un 3904  df-in 3906  df-ss 3916  df-pw 4554  df-sn 4579  df-pr 4581  df-uni 4862  df-pnf 11166

This theorem is referenced by:  pnfnre2  11172  renepnf  11178  ltxrlt  11201  nn0nepnf  12480  xrltnr  13031  pnfnlt  13040  xnn0lenn0nn0  13158  hashclb  14279  hasheq0  14284  pcgcd1  16803  pc2dvds  16805  ramtcl2  16937  odhash3  19503  xrsdsreclblem  21365  pnfnei  23162  iccpnfcnv  24896  i1f0rn  25637