This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem suprltrp

Description: The supremum of a nonempty bounded set of reals can be approximated from below by elements of the set. (Contributed by Glauco Siliprandi, 17-Aug-2020)

		Ref	Expression
	Hypotheses	suprltrp.a	$⊢ φ \to A \subseteq ℝ$
		suprltrp.n0	$⊢ φ \to A \neq \emptyset$
		suprltrp.bnd	$⊢ φ \to \exists x \in ℝ \forall y \in A y \leq x$
		suprltrp.x	$⊢ φ \to X \in ℝ^{+}$
	Assertion	suprltrp	$⊢ φ \to \exists z \in A sup (A ℝ <) - X < z$

Proof

Step	Hyp	Ref	Expression
1		suprltrp.a	$⊢ φ \to A \subseteq ℝ$
2		suprltrp.n0	$⊢ φ \to A \neq \emptyset$
3		suprltrp.bnd	$⊢ φ \to \exists x \in ℝ \forall y \in A y \leq x$
4		suprltrp.x	$⊢ φ \to X \in ℝ^{+}$
5		suprcl	$⊢ (A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \to sup (A ℝ <) \in ℝ$
6	1 2 3 5	syl3anc	$⊢ φ \to sup (A ℝ <) \in ℝ$
7	6 4	ltsubrpd	$⊢ φ \to sup (A ℝ <) - X < sup (A ℝ <)$
8	4	rpred	$⊢ φ \to X \in ℝ$
9	6 8	resubcld	$⊢ φ \to sup (A ℝ <) - X \in ℝ$
10		suprlub	$⊢ ((A \subseteq ℝ \land A \neq \emptyset \land \exists x \in ℝ \forall y \in A y \leq x) \land sup (A ℝ <) - X \in ℝ) \to (sup (A ℝ <) - X < sup (A ℝ <) \leftrightarrow \exists z \in A sup (A ℝ <) - X < z)$
11	1 2 3 9 10	syl31anc	$⊢ φ \to (sup (A ℝ <) - X < sup (A ℝ <) \leftrightarrow \exists z \in A sup (A ℝ <) - X < z)$
12	7 11	mpbid	$⊢ φ \to \exists z \in A sup (A ℝ <) - X < z$