# Metamath Proof Explorer

## Theorem infmrp1

Description: The infimum of the positive reals is 0. (Contributed by AV, 5-Sep-2020)

Ref Expression
Assertion infmrp1 ${⊢}sup\left({ℝ}^{+},ℝ,<\right)=0$

### Proof

Step Hyp Ref Expression
1 rpltrp ${⊢}\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}<{x}$
2 ltso ${⊢}<\mathrm{Or}ℝ$
3 2 a1i ${⊢}\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}<{x}\to <\mathrm{Or}ℝ$
4 0red ${⊢}\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}<{x}\to 0\in ℝ$
5 0red ${⊢}{z}\in {ℝ}^{+}\to 0\in ℝ$
6 rpre ${⊢}{z}\in {ℝ}^{+}\to {z}\in ℝ$
7 rpge0 ${⊢}{z}\in {ℝ}^{+}\to 0\le {z}$
8 5 6 7 lensymd ${⊢}{z}\in {ℝ}^{+}\to ¬{z}<0$
9 8 adantl ${⊢}\left(\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}<{x}\wedge {z}\in {ℝ}^{+}\right)\to ¬{z}<0$
10 elrp ${⊢}{z}\in {ℝ}^{+}↔\left({z}\in ℝ\wedge 0<{z}\right)$
11 breq2 ${⊢}{x}={z}\to \left({y}<{x}↔{y}<{z}\right)$
12 11 rexbidv ${⊢}{x}={z}\to \left(\exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}<{x}↔\exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)$
13 12 rspcv ${⊢}{z}\in {ℝ}^{+}\to \left(\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}<{x}\to \exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)$
14 10 13 sylbir ${⊢}\left({z}\in ℝ\wedge 0<{z}\right)\to \left(\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}<{x}\to \exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}<{z}\right)$
15 14 impcom ${⊢}\left(\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}<{x}\wedge \left({z}\in ℝ\wedge 0<{z}\right)\right)\to \exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}<{z}$
16 3 4 9 15 eqinfd ${⊢}\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{y}<{x}\to sup\left({ℝ}^{+},ℝ,<\right)=0$
17 1 16 ax-mp ${⊢}sup\left({ℝ}^{+},ℝ,<\right)=0$