Description: The positive reals are unbounded above. (Contributed by Mario Carneiro, 7-May-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | rpsup | ⊢ sup ( ℝ+ , ℝ* , < ) = +∞ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ioorp | ⊢ ( 0 (,) +∞ ) = ℝ+ | |
2 | 1 | supeq1i | ⊢ sup ( ( 0 (,) +∞ ) , ℝ* , < ) = sup ( ℝ+ , ℝ* , < ) |
3 | 0xr | ⊢ 0 ∈ ℝ* | |
4 | 0re | ⊢ 0 ∈ ℝ | |
5 | renepnf | ⊢ ( 0 ∈ ℝ → 0 ≠ +∞ ) | |
6 | 4 5 | ax-mp | ⊢ 0 ≠ +∞ |
7 | ioopnfsup | ⊢ ( ( 0 ∈ ℝ* ∧ 0 ≠ +∞ ) → sup ( ( 0 (,) +∞ ) , ℝ* , < ) = +∞ ) | |
8 | 3 6 7 | mp2an | ⊢ sup ( ( 0 (,) +∞ ) , ℝ* , < ) = +∞ |
9 | 2 8 | eqtr3i | ⊢ sup ( ℝ+ , ℝ* , < ) = +∞ |