Metamath Proof Explorer


Theorem pnfnemnf

Description: Plus and minus infinity are different elements of RR* . (Contributed by NM, 14-Oct-2005)

Ref Expression
Assertion pnfnemnf +∞ −∞

Proof

Step Hyp Ref Expression
1 pnfxr +∞ *
2 pwne +∞ * 𝒫 +∞ +∞
3 1 2 ax-mp 𝒫 +∞ +∞
4 3 necomi +∞ 𝒫 +∞
5 df-mnf −∞ = 𝒫 +∞
6 4 5 neeqtrri +∞ −∞