Theorem pnfnre 11276

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

Syntax hints:   ∈ wcel 2108   ∉ wnel 3036  𝒫 cpw 4575  ∪ cuni 4883  ℂcc 11127  ℝcr 11128  +∞cpnf 11266

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-pr 5402  ax-un 7729  ax-resscn 11186

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-nel 3037  df-rab 3416  df-v 3461  df-un 3931  df-in 3933  df-ss 3943  df-pw 4577  df-sn 4602  df-pr 4604  df-uni 4884  df-pnf 11271

This theorem is referenced by:  pnfnre2  11277  renepnf  11283  ltxrlt  11305  nn0nepnf  12582  xrltnr  13135  pnfnlt  13144  xnn0lenn0nn0  13261  hashclb  14376  hasheq0  14381  pcgcd1  16897  pc2dvds  16899  ramtcl2  17031  odhash3  19557  xrsdsreclblem  21380  pnfnei  23158  iccpnfcnv  24893  i1f0rn  25635