Theorem xrge0nemnfd

Description: A nonnegative extended real is not minus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypothesis	xrge0nemnfd.1	|- ( ph -> A e. ( 0 [,] +oo ) )
Assertion	xrge0nemnfd	|- ( ph -> A =/= -oo )

Proof

Step	Hyp	Ref	Expression
1		xrge0nemnfd.1	|- ( ph -> A e. ( 0 [,] +oo ) )
2		mnfxr	|- -oo e. RR*
3	2	a1i	|- ( ph -> -oo e. RR* )
4		iccssxr	|- ( 0 [,] +oo ) C_ RR*
5	4 1	sseldi	|- ( ph -> A e. RR* )
6		0xr	|- 0 e. RR*
7	6	a1i	|- ( ph -> 0 e. RR* )
8		mnflt0	|- -oo < 0
9	8	a1i	|- ( ph -> -oo < 0 )
10		pnfxr	|- +oo e. RR*
11	10	a1i	|- ( ph -> +oo e. RR* )
12		iccgelb	|- ( ( 0 e. RR* /\ +oo e. RR* /\ A e. ( 0 [,] +oo ) ) -> 0 <_ A )
13	7 11 1 12	syl3anc	|- ( ph -> 0 <_ A )
14	3 7 5 9 13	xrltletrd	|- ( ph -> -oo < A )
15	3 5 14	xrgtned	|- ( ph -> A =/= -oo )