Theorem nemnftgtmnft

Description: An extended real that is not minus infinity, is larger than minus infinity. (Contributed by Glauco Siliprandi, 11-Oct-2020)

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

Proof

Step	Hyp	Ref	Expression
1		simpr	|- ( ( A e. RR* /\ A =/= -oo ) -> A =/= -oo )
2	1	neneqd	|- ( ( A e. RR* /\ A =/= -oo ) -> -. A = -oo )
3		ngtmnft	|- ( A e. RR* -> ( A = -oo <-> -. -oo < A ) )
4	3	adantr	|- ( ( A e. RR* /\ A =/= -oo ) -> ( A = -oo <-> -. -oo < A ) )
5	2 4	mtbid	|- ( ( A e. RR* /\ A =/= -oo ) -> -. -. -oo < A )
6		notnotb	|- ( -oo < A <-> -. -. -oo < A )
7	5 6	sylibr	|- ( ( A e. RR* /\ A =/= -oo ) -> -oo < A )