This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nltpnft

Description: An extended real is not less than plus infinity iff they are equal. (Contributed by NM, 30-Jan-2006)

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

Proof

Step Hyp Ref Expression
1 pnfxr 
 |-  +oo e. RR*
2 xrltnr 
 |-  ( +oo e. RR* -> -. +oo < +oo )
3 1 2 ax-mp 
 |-  -. +oo < +oo
4 breq1 
 |-  ( A = +oo -> ( A < +oo <-> +oo < +oo ) )
5 3 4 mtbiri 
 |-  ( A = +oo -> -. A < +oo )
6 pnfge 
 |-  ( A e. RR* -> A <_ +oo )
7 xrleloe 
 |-  ( ( A e. RR* /\ +oo e. RR* ) -> ( A <_ +oo <-> ( A < +oo \/ A = +oo ) ) )
8 1 7 mpan2 
 |-  ( A e. RR* -> ( A <_ +oo <-> ( A < +oo \/ A = +oo ) ) )
9 6 8 mpbid 
 |-  ( A e. RR* -> ( A < +oo \/ A = +oo ) )
10 9 ord 
 |-  ( A e. RR* -> ( -. A < +oo -> A = +oo ) )
11 5 10 impbid2 
 |-  ( A e. RR* -> ( A = +oo <-> -. A < +oo ) )