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