Metamath Proof Explorer


Theorem pnfnre2

Description: Plus infinity is not a real number. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Assertion pnfnre2
|- -. +oo e. RR

Proof

Step Hyp Ref Expression
1 pnfnre
 |-  +oo e/ RR
2 1 neli
 |-  -. +oo e. RR