Theorem pnfnre 11222

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 11217	. . . 4 ⊢ +∞ = 𝒫 ∪ ℂ
2		pwuninel 8257	. . . 4 ⊢ ¬ 𝒫 ∪ ℂ ∈ ℂ
3	1, 2	eqneltri 2848	. . 3 ⊢ ¬ +∞ ∈ ℂ
4		recn 11165	. . 3 ⊢ (+∞ ∈ ℝ → +∞ ∈ ℂ)
5	3, 4	mto 197	. 2 ⊢ ¬ +∞ ∈ ℝ
6	5	nelir 3033	1 ⊢ +∞ ∉ ℝ

Syntax hints:   ∈ wcel 2109   ∉ wnel 3030  𝒫 cpw 4566  ∪ cuni 4874  ℂcc 11073  ℝcr 11074  +∞cpnf 11212

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 2702  ax-sep 5254  ax-pr 5390  ax-un 7714  ax-resscn 11132

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 2709  df-cleq 2722  df-clel 2804  df-nel 3031  df-rab 3409  df-v 3452  df-un 3922  df-in 3924  df-ss 3934  df-pw 4568  df-sn 4593  df-pr 4595  df-uni 4875  df-pnf 11217

This theorem is referenced by:  pnfnre2  11223  renepnf  11229  ltxrlt  11251  nn0nepnf  12530  xrltnr  13086  pnfnlt  13095  xnn0lenn0nn0  13212  hashclb  14330  hasheq0  14335  pcgcd1  16855  pc2dvds  16857  ramtcl2  16989  odhash3  19513  xrsdsreclblem  21336  pnfnei  23114  iccpnfcnv  24849  i1f0rn  25590