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
|- ( ph -> A C_ RR )
suprltrp.n0
|- ( ph -> A =/= (/) )
suprltrp.bnd
|- ( ph -> E. x e. RR A. y e. A y <_ x )
suprltrp.x
|- ( ph -> X e. RR+ )
Assertion suprltrp
|- ( ph -> E. z e. A ( sup ( A , RR , < ) - X ) < z )

Proof

Step Hyp Ref Expression
1 suprltrp.a
 |-  ( ph -> A C_ RR )
2 suprltrp.n0
 |-  ( ph -> A =/= (/) )
3 suprltrp.bnd
 |-  ( ph -> E. x e. RR A. y e. A y <_ x )
4 suprltrp.x
 |-  ( ph -> X e. RR+ )
5 suprcl
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> sup ( A , RR , < ) e. RR )
6 1 2 3 5 syl3anc
 |-  ( ph -> sup ( A , RR , < ) e. RR )
7 6 4 ltsubrpd
 |-  ( ph -> ( sup ( A , RR , < ) - X ) < sup ( A , RR , < ) )
8 4 rpred
 |-  ( ph -> X e. RR )
9 6 8 resubcld
 |-  ( ph -> ( sup ( A , RR , < ) - X ) e. RR )
10 suprlub
 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ ( sup ( A , RR , < ) - X ) e. RR ) -> ( ( sup ( A , RR , < ) - X ) < sup ( A , RR , < ) <-> E. z e. A ( sup ( A , RR , < ) - X ) < z ) )
11 1 2 3 9 10 syl31anc
 |-  ( ph -> ( ( sup ( A , RR , < ) - X ) < sup ( A , RR , < ) <-> E. z e. A ( sup ( A , RR , < ) - X ) < z ) )
12 7 11 mpbid
 |-  ( ph -> E. z e. A ( sup ( A , RR , < ) - X ) < z )