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 )