Theorem pnfnre 11187

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 11182	. . . 4 ⊢ +∞ = 𝒫 ∪ ℂ
2		pwuninel 8229	. . . 4 ⊢ ¬ 𝒫 ∪ ℂ ∈ ℂ
3	1, 2	eqneltri 2856	. . 3 ⊢ ¬ +∞ ∈ ℂ
4		recn 11130	. . 3 ⊢ (+∞ ∈ ℝ → +∞ ∈ ℂ)
5	3, 4	mto 197	. 2 ⊢ ¬ +∞ ∈ ℝ
6	5	nelir 3040	1 ⊢ +∞ ∉ ℝ

Syntax hints:   ∈ wcel 2114   ∉ wnel 3037  𝒫 cpw 4556  ∪ cuni 4865  ℂcc 11038  ℝcr 11039  +∞cpnf 11177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5245  ax-pr 5381  ax-un 7692  ax-resscn 11097

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nel 3038  df-rab 3402  df-v 3444  df-un 3908  df-in 3910  df-ss 3920  df-pw 4558  df-sn 4583  df-pr 4585  df-uni 4866  df-pnf 11182

This theorem is referenced by:  pnfnre2  11188  renepnf  11194  ltxrlt  11217  nn0nepnf  12496  xrltnr  13047  pnfnlt  13056  xnn0lenn0nn0  13174  hashclb  14295  hasheq0  14300  pcgcd1  16819  pc2dvds  16821  ramtcl2  16953  odhash3  19522  xrsdsreclblem  21384  pnfnei  23181  iccpnfcnv  24915  i1f0rn  25656