Theorem ge0nemnf

Description: A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015)

	Ref	Expression
Assertion	ge0nemnf	|- ( ( A e. RR* /\ 0 <_ A ) -> A =/= -oo )

Proof

Step	Hyp	Ref	Expression
1		ge0gtmnf	|- ( ( A e. RR* /\ 0 <_ A ) -> -oo < A )
2		ngtmnft	|- ( A e. RR* -> ( A = -oo <-> -. -oo < A ) )
3	2	adantr	|- ( ( A e. RR* /\ 0 <_ A ) -> ( A = -oo <-> -. -oo < A ) )
4	3	necon2abid	|- ( ( A e. RR* /\ 0 <_ A ) -> ( -oo < A <-> A =/= -oo ) )
5	1 4	mpbid	|- ( ( A e. RR* /\ 0 <_ A ) -> A =/= -oo )