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

Metamath Proof Explorer

Theorem renepnf

Description: No (finite) real equals plus infinity. (Contributed by NM, 14-Oct-2005) (Proof shortened by Andrew Salmon, 19-Nov-2011)

		Ref	Expression
	Assertion	renepnf	$⊢ A \in ℝ \to A \neq +∞$

Step	Hyp	Ref	Expression
1		pnfnre	$⊢ +∞ \notin ℝ$
2	1	neli	$⊢ \neg +∞ \in ℝ$
3		eleq1	$⊢ A = +∞ \to (A \in ℝ \leftrightarrow +∞ \in ℝ)$
4	2 3	mtbiri	$⊢ A = +∞ \to \neg A \in ℝ$
5	4	necon2ai	$⊢ A \in ℝ \to A \neq +∞$