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

Metamath Proof Explorer

Theorem mnfnre

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

		Ref	Expression
	Assertion	mnfnre	$⊢ −∞ \notin ℝ$

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