Theorem pnfnre 10705

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 10700	. . . 4 ⊢ +∞ = 𝒫 ∪ ℂ
2		pwuninel 7944	. . . 4 ⊢ ¬ 𝒫 ∪ ℂ ∈ ℂ
3	1, 2	eqneltri 2844	. . 3 ⊢ ¬ +∞ ∈ ℂ
4		recn 10650	. . 3 ⊢ (+∞ ∈ ℝ → +∞ ∈ ℂ)
5	3, 4	mto 200	. 2 ⊢ ¬ +∞ ∈ ℝ
6	5	nelir 3056	1 ⊢ +∞ ∉ ℝ

Syntax hints:   ∈ wcel 2112   ∉ wnel 3053  𝒫 cpw 4487  ∪ cuni 4791  ℂcc 10558  ℝcr 10559  +∞cpnf 10695

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730  ax-sep 5162  ax-nul 5169  ax-pr 5291  ax-un 7452  ax-resscn 10617

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-tru 1542  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-nel 3054  df-rab 3077  df-v 3409  df-dif 3857  df-un 3859  df-in 3861  df-ss 3871  df-nul 4222  df-pw 4489  df-sn 4516  df-pr 4518  df-uni 4792  df-pnf 10700

This theorem is referenced by:  pnfnre2  10706  renepnf  10712  ltxrlt  10734  nn0nepnf  11999  xrltnr  12540  pnfnlt  12549  xnn0lenn0nn0  12664  hashclb  13754  hasheq0  13759  pcgcd1  16253  pc2dvds  16255  ramtcl2  16387  odhash3  18753  xrsdsreclblem  20197  pnfnei  21905  iccpnfcnv  23630  i1f0rn  24367