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	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	suprltrp.n0	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
	suprltrp.bnd	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
	suprltrp.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ+ )
Assertion	suprltrp	⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝐴 ( sup ( 𝐴 , ℝ , < ) − 𝑋 ) < 𝑧 )

Proof

Step	Hyp	Ref	Expression
1		suprltrp.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2		suprltrp.n0	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
3		suprltrp.bnd	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
4		suprltrp.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ+ )
5		suprcl	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → sup ( 𝐴 , ℝ , < ) ∈ ℝ )
6	1 2 3 5	syl3anc	⊢ ( 𝜑 → sup ( 𝐴 , ℝ , < ) ∈ ℝ )
7	6 4	ltsubrpd	⊢ ( 𝜑 → ( sup ( 𝐴 , ℝ , < ) − 𝑋 ) < sup ( 𝐴 , ℝ , < ) )
8	4	rpred	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
9	6 8	resubcld	⊢ ( 𝜑 → ( sup ( 𝐴 , ℝ , < ) − 𝑋 ) ∈ ℝ )
10		suprlub	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ ( sup ( 𝐴 , ℝ , < ) − 𝑋 ) ∈ ℝ ) → ( ( sup ( 𝐴 , ℝ , < ) − 𝑋 ) < sup ( 𝐴 , ℝ , < ) ↔ ∃ 𝑧 ∈ 𝐴 ( sup ( 𝐴 , ℝ , < ) − 𝑋 ) < 𝑧 ) )
11	1 2 3 9 10	syl31anc	⊢ ( 𝜑 → ( ( sup ( 𝐴 , ℝ , < ) − 𝑋 ) < sup ( 𝐴 , ℝ , < ) ↔ ∃ 𝑧 ∈ 𝐴 ( sup ( 𝐴 , ℝ , < ) − 𝑋 ) < 𝑧 ) )
12	7 11	mpbid	⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝐴 ( sup ( 𝐴 , ℝ , < ) − 𝑋 ) < 𝑧 )