Theorem pnfnre 10398

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		pwuninel 7666	. . . 4 ⊢ ¬ 𝒫 ∪ ℂ ∈ ℂ
2		df-pnf 10393	. . . . 5 ⊢ +∞ = 𝒫 ∪ ℂ
3	2	eleq1i 2897	. . . 4 ⊢ (+∞ ∈ ℂ ↔ 𝒫 ∪ ℂ ∈ ℂ)
4	1, 3	mtbir 315	. . 3 ⊢ ¬ +∞ ∈ ℂ
5		recn 10342	. . 3 ⊢ (+∞ ∈ ℝ → +∞ ∈ ℂ)
6	4, 5	mto 189	. 2 ⊢ ¬ +∞ ∈ ℝ
7	6	nelir 3105	1 ⊢ +∞ ∉ ℝ

Syntax hints:   ∈ wcel 2166   ∉ wnel 3102  𝒫 cpw 4378  ∪ cuni 4658  ℂcc 10250  ℝcr 10251  +∞cpnf 10388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pr 5127  ax-un 7209  ax-resscn 10309

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-nel 3103  df-rex 3123  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-pw 4380  df-sn 4398  df-pr 4400  df-uni 4659  df-pnf 10393

This theorem is referenced by:  renepnf  10404  ltxrlt  10427  nn0nepnf  11698  xrltnr  12239  pnfnlt  12248  xnn0lenn0nn0  12363  hashclb  13439  hasheq0  13444  pcgcd1  15952  pc2dvds  15954  ramtcl2  16086  odhash3  18342  xrsdsreclblem  20152  pnfnei  21395  iccpnfcnv  23113  i1f0rn  23848  pnfnre2  40423