Theorem mnfnre

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

	Ref	Expression
Assertion	mnfnre	$$⊢\mathrm{-\infty }\notin ℝ$$

Proof

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