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	⊢ ( 𝐴 ∈ ℝ → 𝐴 ≠ +∞ )

Proof

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