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 
|- ( 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 )