Theorem pnfnre 11300

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 11295	. . . 4 ⊢ +∞ = 𝒫 ∪ ℂ
2		pwuninel 8299	. . . 4 ⊢ ¬ 𝒫 ∪ ℂ ∈ ℂ
3	1, 2	eqneltri 2858	. . 3 ⊢ ¬ +∞ ∈ ℂ
4		recn 11243	. . 3 ⊢ (+∞ ∈ ℝ → +∞ ∈ ℂ)
5	3, 4	mto 197	. 2 ⊢ ¬ +∞ ∈ ℝ
6	5	nelir 3047	1 ⊢ +∞ ∉ ℝ

Syntax hints:   ∈ wcel 2106   ∉ wnel 3044  𝒫 cpw 4605  ∪ cuni 4912  ℂcc 11151  ℝcr 11152  +∞cpnf 11290

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-pr 5438  ax-un 7754  ax-resscn 11210

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-nel 3045  df-rab 3434  df-v 3480  df-un 3968  df-in 3970  df-ss 3980  df-pw 4607  df-sn 4632  df-pr 4634  df-uni 4913  df-pnf 11295

This theorem is referenced by:  pnfnre2  11301  renepnf  11307  ltxrlt  11329  nn0nepnf  12605  xrltnr  13159  pnfnlt  13168  xnn0lenn0nn0  13284  hashclb  14394  hasheq0  14399  pcgcd1  16911  pc2dvds  16913  ramtcl2  17045  odhash3  19609  xrsdsreclblem  21448  pnfnei  23244  iccpnfcnv  24989  i1f0rn  25731