Description: The positive reals are unbounded above. (Contributed by Mario Carneiro, 7-May-2016)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | rpsup | |- sup ( RR+ , RR* , < ) = +oo |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ioorp | |- ( 0 (,) +oo ) = RR+ |
|
| 2 | 1 | supeq1i | |- sup ( ( 0 (,) +oo ) , RR* , < ) = sup ( RR+ , RR* , < ) |
| 3 | 0xr | |- 0 e. RR* |
|
| 4 | 0re | |- 0 e. RR |
|
| 5 | renepnf | |- ( 0 e. RR -> 0 =/= +oo ) |
|
| 6 | 4 5 | ax-mp | |- 0 =/= +oo |
| 7 | ioopnfsup | |- ( ( 0 e. RR* /\ 0 =/= +oo ) -> sup ( ( 0 (,) +oo ) , RR* , < ) = +oo ) |
|
| 8 | 3 6 7 | mp2an | |- sup ( ( 0 (,) +oo ) , RR* , < ) = +oo |
| 9 | 2 8 | eqtr3i | |- sup ( RR+ , RR* , < ) = +oo |