Theorem pnfnre 11163

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

Syntax hints:   ∈ wcel 2113   ∉ wnel 3034  𝒫 cpw 4551  ∪ cuni 4860  ℂcc 11014  ℝcr 11015  +∞cpnf 11153

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 2705  ax-sep 5238  ax-pr 5374  ax-un 7677  ax-resscn 11073

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 2712  df-cleq 2725  df-clel 2808  df-nel 3035  df-rab 3398  df-v 3440  df-un 3904  df-in 3906  df-ss 3916  df-pw 4553  df-sn 4578  df-pr 4580  df-uni 4861  df-pnf 11158

This theorem is referenced by:  pnfnre2  11164  renepnf  11170  ltxrlt  11193  nn0nepnf  12472  xrltnr  13028  pnfnlt  13037  xnn0lenn0nn0  13154  hashclb  14275  hasheq0  14280  pcgcd1  16799  pc2dvds  16801  ramtcl2  16933  odhash3  19498  xrsdsreclblem  21359  pnfnei  23145  iccpnfcnv  24879  i1f0rn  25620