Metamath Proof Explorer

Theorem ge0gtmnf

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

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

Proof

Step Hyp Ref Expression
1 mnflt0 
 |-  -oo < 0
2 mnfxr 
 |-  -oo e. RR*
3 0xr 
 |-  0 e. RR*
4 xrltletr 
 |-  ( ( -oo e. RR* /\ 0 e. RR* /\ A e. RR* ) -> ( ( -oo < 0 /\ 0 <_ A ) -> -oo < A ) )
5 2 3 4 mp3an12 
 |-  ( A e. RR* -> ( ( -oo < 0 /\ 0 <_ A ) -> -oo < A ) )
6 5 imp 
 |-  ( ( A e. RR* /\ ( -oo < 0 /\ 0 <_ A ) ) -> -oo < A )
7 1 6 mpanr1 
 |-  ( ( A e. RR* /\ 0 <_ A ) -> -oo < A )