This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pnfnre

Description: Plus infinity is not a real number. (Contributed by NM, 13-Oct-2005)

		Ref	Expression
	Assertion	pnfnre	$⊢ +∞ \notin ℝ$

Step	Hyp	Ref	Expression
1		df-pnf	$⊢ +∞ = 𝒫 ⋃ ℂ$
2		pwuninel	$⊢ \neg 𝒫 ⋃ ℂ \in ℂ$
3	1 2	eqneltri	$⊢ \neg +∞ \in ℂ$
4		recn	$⊢ +∞ \in ℝ \to +∞ \in ℂ$
5	3 4	mto	$⊢ \neg +∞ \in ℝ$
6	5	nelir	$⊢ +∞ \notin ℝ$