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 φA
suprltrp.n0 φA
suprltrp.bnd φxyAyx
suprltrp.x φX+
Assertion suprltrp φzAsupA<X<z

Proof

Step Hyp Ref Expression
1 suprltrp.a φA
2 suprltrp.n0 φA
3 suprltrp.bnd φxyAyx
4 suprltrp.x φX+
5 suprcl AAxyAyxsupA<
6 1 2 3 5 syl3anc φsupA<
7 6 4 ltsubrpd φsupA<X<supA<
8 4 rpred φX
9 6 8 resubcld φsupA<X
10 suprlub AAxyAyxsupA<XsupA<X<supA<zAsupA<X<z
11 1 2 3 9 10 syl31anc φsupA<X<supA<zAsupA<X<z
12 7 11 mpbid φzAsupA<X<z