Metamath Proof Explorer

Theorem xgepnf

Description: An extended real which is greater than plus infinity is plus infinity. (Contributed by Thierry Arnoux, 18-Dec-2016)

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

Proof

Step Hyp Ref Expression
1 pnfxr 
 |-  +oo e. RR*
2 xrlenlt 
 |-  ( ( +oo e. RR* /\ A e. RR* ) -> ( +oo <_ A <-> -. A < +oo ) )
3 1 2 mpan 
 |-  ( A e. RR* -> ( +oo <_ A <-> -. A < +oo ) )
4 nltpnft 
 |-  ( A e. RR* -> ( A = +oo <-> -. A < +oo ) )
5 3 4 bitr4d 
 |-  ( A e. RR* -> ( +oo <_ A <-> A = +oo ) )