Theorem pnfnre 10947

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 10942	. . . 4 ⊢ +∞ = 𝒫 ∪ ℂ
2		pwuninel 8062	. . . 4 ⊢ ¬ 𝒫 ∪ ℂ ∈ ℂ
3	1, 2	eqneltri 2832	. . 3 ⊢ ¬ +∞ ∈ ℂ
4		recn 10892	. . 3 ⊢ (+∞ ∈ ℝ → +∞ ∈ ℂ)
5	3, 4	mto 196	. 2 ⊢ ¬ +∞ ∈ ℝ
6	5	nelir 3051	1 ⊢ +∞ ∉ ℝ

Syntax hints:   ∈ wcel 2108   ∉ wnel 3048  𝒫 cpw 4530  ∪ cuni 4836  ℂcc 10800  ℝcr 10801  +∞cpnf 10937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566  ax-resscn 10859

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-nel 3049  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-pw 4532  df-sn 4559  df-pr 4561  df-uni 4837  df-pnf 10942

This theorem is referenced by:  pnfnre2  10948  renepnf  10954  ltxrlt  10976  nn0nepnf  12243  xrltnr  12784  pnfnlt  12793  xnn0lenn0nn0  12908  hashclb  14001  hasheq0  14006  pcgcd1  16506  pc2dvds  16508  ramtcl2  16640  odhash3  19096  xrsdsreclblem  20556  pnfnei  22279  iccpnfcnv  24013  i1f0rn  24751