Metamath Proof Explorer

Theorem pnfge

Description: Plus infinity is an upper bound for extended reals. (Contributed by NM, 30-Jan-2006)

Ref Expression
Assertion pnfge 
|- ( A e. RR* -> A <_ +oo )

Proof

Step Hyp Ref Expression
1 pnfnlt 
 |-  ( A e. RR* -> -. +oo < A )
2 pnfxr 
 |-  +oo e. RR*
3 xrlenlt 
 |-  ( ( A e. RR* /\ +oo e. RR* ) -> ( A <_ +oo <-> -. +oo < A ) )
4 2 3 mpan2 
 |-  ( A e. RR* -> ( A <_ +oo <-> -. +oo < A ) )
5 1 4 mpbird 
 |-  ( A e. RR* -> A <_ +oo )