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

Proof

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