Theorem pnfnre 11256

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 11251	. . . 4 ⊢ +∞ = 𝒫 ∪ ℂ
2		pwuninel 8269	. . . 4 ⊢ ¬ 𝒫 ∪ ℂ ∈ ℂ
3	1, 2	eqneltri 2881	. . 3 ⊢ ¬ +∞ ∈ ℂ
4		recn 11196	. . 3 ⊢ (+∞ ∈ ℝ → +∞ ∈ ℂ)
5	3, 4	mto 200	. 2 ⊢ ¬ +∞ ∈ ℝ
6	5	nelir 3066	1 ⊢ +∞ ∉ ℝ

This proof depends on syntax axioms:   ∈ wcel 2142   ∉ wnel 3063  𝒫 cpw 4561  ∪ cuni 4871  ℂcc 11104  ℝcr 11105  +∞cpnf 11246

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5256  ax-resscn 11163

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1104  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-nel 3064  df-rab 3416  df-v 3456  df-in 3911  df-ss 3921  df-pw 4563  df-uni 4872  df-pnf 11251

This theorem is used by:  pnfnre2  11257  renepnf  11263  ltxrlt  11286  nn0nepnf  12591  xrltnr  13150  pnfnlt  13159  xnn0lenn0nn0  13277  hashclb  14401  hasheq0  14406  pcgcd1  16943  pc2dvds  16945  ramtcl2  17077  odhash3  19652  xrsdsreclblem  21574  pnfnei  23388  iccpnfcnv  25114  i1f0rn  25852