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 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
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 ( 𝐴 , ℝ , < ) − 𝑋 ) < 𝑧 )