Metamath Proof Explorer


Theorem rpsup

Description: The positive reals are unbounded above. (Contributed by Mario Carneiro, 7-May-2016)

Ref Expression
Assertion rpsup sup ( ℝ+ , ℝ* , < ) = +∞

Proof

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 ( ℝ+ , ℝ* , < ) = +∞