Theorem pnfnre 11183

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

Syntax hints:   ∈ wcel 2114   ∉ wnel 3037  𝒫 cpw 4542  ∪ cuni 4851  ℂcc 11033  ℝcr 11034  +∞cpnf 11173

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 5232  ax-pr 5374  ax-un 7686  ax-resscn 11092

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 3391  df-v 3432  df-un 3895  df-in 3897  df-ss 3907  df-pw 4544  df-sn 4569  df-pr 4571  df-uni 4852  df-pnf 11178

This theorem is referenced by:  pnfnre2  11184  renepnf  11190  ltxrlt  11213  nn0nepnf  12515  xrltnr  13067  pnfnlt  13076  xnn0lenn0nn0  13194  hashclb  14317  hasheq0  14322  pcgcd1  16845  pc2dvds  16847  ramtcl2  16979  odhash3  19548  xrsdsreclblem  21408  pnfnei  23201  iccpnfcnv  24927  i1f0rn  25665