Theorem pnfnre

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

	Ref	Expression
Assertion	pnfnre	$$⊢\mathrm{+\infty }\notin ℝ$$

Proof

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