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