Theorem infmrp1

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

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

Proof

Step	Hyp	Ref	Expression
1		rpltrp	$$⊢\forall x\in {ℝ}^{+}\exists y\in {ℝ}^{+}y<x$$
2		ltso	$$⊢<\mathrm{Or}ℝ$$
3	2	a1i	$$⊢\forall x\in {ℝ}^{+}\exists y\in {ℝ}^{+}y<x\to <\mathrm{Or}ℝ$$
4		0red	$$⊢\forall x\in {ℝ}^{+}\exists y\in {ℝ}^{+}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 \neg z<0$$
9	8	adantl	$$⊢\left(\forall x\in {ℝ}^{+}\exists y\in {ℝ}^{+}y<x\wedge z\in {ℝ}^{+}\right)\to \neg z<0$$
10		elrp	$$⊢z\in {ℝ}^{+}\leftrightarrow \left(z\in ℝ\wedge 0<z\right)$$
11		breq2	$$⊢x=z\to \left(y<x\leftrightarrow y<z\right)$$
12	11	rexbidv	$$⊢x=z\to \left(\exists y\in {ℝ}^{+}y<x\leftrightarrow \exists y\in {ℝ}^{+}y<z\right)$$
13	12	rspcv	$$⊢z\in {ℝ}^{+}\to \left(\forall x\in {ℝ}^{+}\exists y\in {ℝ}^{+}y<x\to \exists y\in {ℝ}^{+}y<z\right)$$
14	10 13	sylbir	$$⊢\left(z\in ℝ\wedge 0<z\right)\to \left(\forall x\in {ℝ}^{+}\exists y\in {ℝ}^{+}y<x\to \exists y\in {ℝ}^{+}y<z\right)$$
15	14	impcom	$$⊢\left(\forall x\in {ℝ}^{+}\exists y\in {ℝ}^{+}y<x\wedge \left(z\in ℝ\wedge 0<z\right)\right)\to \exists y\in {ℝ}^{+}y<z$$
16	3 4 9 15	eqinfd	$$⊢\forall x\in {ℝ}^{+}\exists y\in {ℝ}^{+}y<x\to inf\left({ℝ}^{+},ℝ,<\right)=0$$
17	1 16	ax-mp	$$⊢inf\left({ℝ}^{+},ℝ,<\right)=0$$