Description: A nonnegative extended real is not equal to minus infinity. (Contributed by Thierry Arnoux, 9-Jun-2017) (Proof shortened by Glauco Siliprandi, 17-Aug-2020)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | xrge0neqmnf | |- ( A e. ( 0 [,] +oo ) -> A =/= -oo ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eliccxr | |- ( A e. ( 0 [,] +oo ) -> A e. RR* ) |
|
| 2 | 0xr | |- 0 e. RR* |
|
| 3 | pnfxr | |- +oo e. RR* |
|
| 4 | iccgelb | |- ( ( 0 e. RR* /\ +oo e. RR* /\ A e. ( 0 [,] +oo ) ) -> 0 <_ A ) |
|
| 5 | 2 3 4 | mp3an12 | |- ( A e. ( 0 [,] +oo ) -> 0 <_ A ) |
| 6 | ge0nemnf | |- ( ( A e. RR* /\ 0 <_ A ) -> A =/= -oo ) |
|
| 7 | 1 5 6 | syl2anc | |- ( A e. ( 0 [,] +oo ) -> A =/= -oo ) |