Theorem pnfnre 11156

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 11151	. . . 4 ⊢ +∞ = 𝒫 ∪ ℂ
2		pwuninel 8208	. . . 4 ⊢ ¬ 𝒫 ∪ ℂ ∈ ℂ
3	1, 2	eqneltri 2847	. . 3 ⊢ ¬ +∞ ∈ ℂ
4		recn 11099	. . 3 ⊢ (+∞ ∈ ℝ → +∞ ∈ ℂ)
5	3, 4	mto 197	. 2 ⊢ ¬ +∞ ∈ ℝ
6	5	nelir 3032	1 ⊢ +∞ ∉ ℝ

Syntax hints:   ∈ wcel 2109   ∉ wnel 3029  𝒫 cpw 4551  ∪ cuni 4858  ℂcc 11007  ℝcr 11008  +∞cpnf 11146

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-pr 5371  ax-un 7671  ax-resscn 11066

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nel 3030  df-rab 3395  df-v 3438  df-un 3908  df-in 3910  df-ss 3920  df-pw 4553  df-sn 4578  df-pr 4580  df-uni 4859  df-pnf 11151

This theorem is referenced by:  pnfnre2  11157  renepnf  11163  ltxrlt  11186  nn0nepnf  12465  xrltnr  13021  pnfnlt  13030  xnn0lenn0nn0  13147  hashclb  14265  hasheq0  14270  pcgcd1  16789  pc2dvds  16791  ramtcl2  16923  odhash3  19455  xrsdsreclblem  21319  pnfnei  23105  iccpnfcnv  24840  i1f0rn  25581