Theorem pnfnre 11181

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 11176	. . . 4 ⊢ +∞ = 𝒫 ∪ ℂ
2		pwuninel 8219	. . . 4 ⊢ ¬ 𝒫 ∪ ℂ ∈ ℂ
3	1, 2	eqneltri 2860	. . 3 ⊢ ¬ +∞ ∈ ℂ
4		recn 11123	. . 3 ⊢ (+∞ ∈ ℝ → +∞ ∈ ℂ)
5	3, 4	mto 199	. 2 ⊢ ¬ +∞ ∈ ℝ
6	5	nelir 3043	1 ⊢ +∞ ∉ ℝ

Syntax hints:   ∈ wcel 2121   ∉ wnel 3040  𝒫 cpw 4532  ∪ cuni 4841  ℂcc 11031  ℝcr 11032  +∞cpnf 11171

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5221  ax-pr 5365  ax-un 7682  ax-resscn 11090

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-nel 3041  df-rab 3394  df-v 3435  df-un 3890  df-in 3892  df-ss 3902  df-pw 4534  df-sn 4559  df-pr 4561  df-uni 4842  df-pnf 11176

This theorem is referenced by:  pnfnre2  11182  renepnf  11188  ltxrlt  11211  nn0nepnf  12513  xrltnr  13065  pnfnlt  13074  xnn0lenn0nn0  13192  hashclb  14315  hasheq0  14320  pcgcd1  16843  pc2dvds  16845  ramtcl2  16977  odhash3  19546  xrsdsreclblem  21392  pnfnei  23207  iccpnfcnv  24933  i1f0rn  25671