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

Proof

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