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

Metamath Proof Explorer

Theorem pnfnemnf

Description: Plus and minus infinity are different elements of RR* . (Contributed by NM, 14-Oct-2005)

		Ref	Expression
	Assertion	pnfnemnf	$⊢ +∞ \neq −∞$

Step	Hyp	Ref	Expression
1		pnfxr	$⊢ +∞ \in ℝ^{*}$
2		pwne	$⊢ +∞ \in ℝ^{*} \to 𝒫 +∞ \neq +∞$
3	1 2	ax-mp	$⊢ 𝒫 +∞ \neq +∞$
4	3	necomi	$⊢ +∞ \neq 𝒫 +∞$
5		df-mnf	$⊢ −∞ = 𝒫 +∞$
6	4 5	neeqtrri	$⊢ +∞ \neq −∞$