Theorem pnfnre 11331

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 11326	. . . 4 ⊢ +∞ = 𝒫 ∪ ℂ
2		pwuninel 8316	. . . 4 ⊢ ¬ 𝒫 ∪ ℂ ∈ ℂ
3	1, 2	eqneltri 2863	. . 3 ⊢ ¬ +∞ ∈ ℂ
4		recn 11274	. . 3 ⊢ (+∞ ∈ ℝ → +∞ ∈ ℂ)
5	3, 4	mto 197	. 2 ⊢ ¬ +∞ ∈ ℝ
6	5	nelir 3055	1 ⊢ +∞ ∉ ℝ

Syntax hints:   ∈ wcel 2108   ∉ wnel 3052  𝒫 cpw 4622  ∪ cuni 4931  ℂcc 11182  ℝcr 11183  +∞cpnf 11321

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-pr 5447  ax-un 7770  ax-resscn 11241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-nel 3053  df-rab 3444  df-v 3490  df-un 3981  df-in 3983  df-ss 3993  df-pw 4624  df-sn 4649  df-pr 4651  df-uni 4932  df-pnf 11326

This theorem is referenced by:  pnfnre2  11332  renepnf  11338  ltxrlt  11360  nn0nepnf  12633  xrltnr  13182  pnfnlt  13191  xnn0lenn0nn0  13307  hashclb  14407  hasheq0  14412  pcgcd1  16924  pc2dvds  16926  ramtcl2  17058  odhash3  19618  xrsdsreclblem  21453  pnfnei  23249  iccpnfcnv  24994  i1f0rn  25736