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