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 | |
|
suprltrp.n0 | |
||
suprltrp.bnd | |
||
suprltrp.x | |
||
Assertion | suprltrp | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | suprltrp.a | |
|
2 | suprltrp.n0 | |
|
3 | suprltrp.bnd | |
|
4 | suprltrp.x | |
|
5 | suprcl | |
|
6 | 1 2 3 5 | syl3anc | |
7 | 6 4 | ltsubrpd | |
8 | 4 | rpred | |
9 | 6 8 | resubcld | |
10 | suprlub | |
|
11 | 1 2 3 9 10 | syl31anc | |
12 | 7 11 | mpbid | |