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 ) )