Description: The supremum of a bounded-above set of reals is the negation of the infimum of that set's image under negation. (Contributed by Paul Chapman, 21-Mar-2011) ( Revised by AV, 13-Sep-2020.)
Ref | Expression | ||
---|---|---|---|
Assertion | supminf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssrab2 | |
|
2 | negn0 | |
|
3 | ublbneg | |
|
4 | infrenegsup | |
|
5 | 1 2 3 4 | mp3an3an | |
6 | 5 | 3impa | |
7 | elrabi | |
|
8 | 7 | adantl | |
9 | ssel2 | |
|
10 | negeq | |
|
11 | 10 | eleq1d | |
12 | 11 | elrab3 | |
13 | renegcl | |
|
14 | negeq | |
|
15 | 14 | eleq1d | |
16 | 15 | elrab3 | |
17 | 13 16 | syl | |
18 | recn | |
|
19 | 18 | negnegd | |
20 | 19 | eleq1d | |
21 | 12 17 20 | 3bitrd | |
22 | 21 | adantl | |
23 | 8 9 22 | eqrdav | |
24 | 23 | supeq1d | |
25 | 24 | 3ad2ant1 | |
26 | 25 | negeqd | |
27 | 6 26 | eqtrd | |
28 | infrecl | |
|
29 | 1 2 3 28 | mp3an3an | |
30 | 29 | 3impa | |
31 | suprcl | |
|
32 | recn | |
|
33 | recn | |
|
34 | negcon2 | |
|
35 | 32 33 34 | syl2an | |
36 | 30 31 35 | syl2anc | |
37 | 27 36 | mpbid | |