Theorem pnfnre 11177

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

Syntax hints:   ∈ wcel 2114   ∉ wnel 3037  𝒫 cpw 4555  ∪ cuni 4864  ℂcc 11028  ℝcr 11029  +∞cpnf 11167

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 5242  ax-pr 5378  ax-un 7682  ax-resscn 11087

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 3401  df-v 3443  df-un 3907  df-in 3909  df-ss 3919  df-pw 4557  df-sn 4582  df-pr 4584  df-uni 4865  df-pnf 11172

This theorem is referenced by:  pnfnre2  11178  renepnf  11184  ltxrlt  11207  nn0nepnf  12486  xrltnr  13037  pnfnlt  13046  xnn0lenn0nn0  13164  hashclb  14285  hasheq0  14290  pcgcd1  16809  pc2dvds  16811  ramtcl2  16943  odhash3  19509  xrsdsreclblem  21371  pnfnei  23168  iccpnfcnv  24902  i1f0rn  25643