Metamath Proof Explorer

Theorem pnfel0pnf

Description: +oo is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion pnfel0pnf 
|- +oo e. ( 0 [,] +oo )

Proof

Step Hyp Ref Expression
1 0xr 
 |-  0 e. RR*
2 pnfxr 
 |-  +oo e. RR*
3 0lepnf 
 |-  0 <_ +oo
4 ubicc2 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ 0 <_ +oo ) -> +oo e. ( 0 [,] +oo ) )
5 1 2 3 4 mp3an 
 |-  +oo e. ( 0 [,] +oo )