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

Metamath Proof Explorer

Theorem renemnf

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

		Ref	Expression
	Assertion	renemnf	⊢ ( 𝐴 ∈ ℝ → 𝐴 ≠ -∞ )

Step	Hyp	Ref	Expression
1		mnfnre	⊢ -∞ ∉ ℝ
2	1	neli	⊢ ¬ -∞ ∈ ℝ
3		eleq1	⊢ ( 𝐴 = -∞ → ( 𝐴 ∈ ℝ ↔ -∞ ∈ ℝ ) )
4	2 3	mtbiri	⊢ ( 𝐴 = -∞ → ¬ 𝐴 ∈ ℝ )
5	4	necon2ai	⊢ ( 𝐴 ∈ ℝ → 𝐴 ≠ -∞ )