Step |
Hyp |
Ref |
Expression |
1 |
|
supminfxr2.1 |
|- ( ph -> A C_ RR* ) |
2 |
|
xnegmnf |
|- -e -oo = +oo |
3 |
2
|
eqcomi |
|- +oo = -e -oo |
4 |
3
|
a1i |
|- ( ( ph /\ +oo e. A ) -> +oo = -e -oo ) |
5 |
|
supxrpnf |
|- ( ( A C_ RR* /\ +oo e. A ) -> sup ( A , RR* , < ) = +oo ) |
6 |
1 5
|
sylan |
|- ( ( ph /\ +oo e. A ) -> sup ( A , RR* , < ) = +oo ) |
7 |
|
ssrab2 |
|- { y e. RR* | -e y e. A } C_ RR* |
8 |
7
|
a1i |
|- ( +oo e. A -> { y e. RR* | -e y e. A } C_ RR* ) |
9 |
|
xnegeq |
|- ( y = -oo -> -e y = -e -oo ) |
10 |
2
|
a1i |
|- ( y = -oo -> -e -oo = +oo ) |
11 |
9 10
|
eqtrd |
|- ( y = -oo -> -e y = +oo ) |
12 |
11
|
eleq1d |
|- ( y = -oo -> ( -e y e. A <-> +oo e. A ) ) |
13 |
|
mnfxr |
|- -oo e. RR* |
14 |
13
|
a1i |
|- ( +oo e. A -> -oo e. RR* ) |
15 |
|
id |
|- ( +oo e. A -> +oo e. A ) |
16 |
12 14 15
|
elrabd |
|- ( +oo e. A -> -oo e. { y e. RR* | -e y e. A } ) |
17 |
|
infxrmnf |
|- ( ( { y e. RR* | -e y e. A } C_ RR* /\ -oo e. { y e. RR* | -e y e. A } ) -> inf ( { y e. RR* | -e y e. A } , RR* , < ) = -oo ) |
18 |
8 16 17
|
syl2anc |
|- ( +oo e. A -> inf ( { y e. RR* | -e y e. A } , RR* , < ) = -oo ) |
19 |
18
|
adantl |
|- ( ( ph /\ +oo e. A ) -> inf ( { y e. RR* | -e y e. A } , RR* , < ) = -oo ) |
20 |
19
|
xnegeqd |
|- ( ( ph /\ +oo e. A ) -> -e inf ( { y e. RR* | -e y e. A } , RR* , < ) = -e -oo ) |
21 |
4 6 20
|
3eqtr4d |
|- ( ( ph /\ +oo e. A ) -> sup ( A , RR* , < ) = -e inf ( { y e. RR* | -e y e. A } , RR* , < ) ) |
22 |
1
|
ssdifssd |
|- ( ph -> ( A \ { -oo } ) C_ RR* ) |
23 |
22
|
adantr |
|- ( ( ph /\ -. +oo e. A ) -> ( A \ { -oo } ) C_ RR* ) |
24 |
|
difssd |
|- ( -. +oo e. A -> ( A \ { -oo } ) C_ A ) |
25 |
|
id |
|- ( -. +oo e. A -> -. +oo e. A ) |
26 |
|
ssnel |
|- ( ( ( A \ { -oo } ) C_ A /\ -. +oo e. A ) -> -. +oo e. ( A \ { -oo } ) ) |
27 |
24 25 26
|
syl2anc |
|- ( -. +oo e. A -> -. +oo e. ( A \ { -oo } ) ) |
28 |
27
|
adantl |
|- ( ( ph /\ -. +oo e. A ) -> -. +oo e. ( A \ { -oo } ) ) |
29 |
|
neldifsnd |
|- ( ( ph /\ -. +oo e. A ) -> -. -oo e. ( A \ { -oo } ) ) |
30 |
23 28 29
|
xrssre |
|- ( ( ph /\ -. +oo e. A ) -> ( A \ { -oo } ) C_ RR ) |
31 |
30
|
supminfxr |
|- ( ( ph /\ -. +oo e. A ) -> sup ( ( A \ { -oo } ) , RR* , < ) = -e inf ( { y e. RR | -u y e. ( A \ { -oo } ) } , RR* , < ) ) |
32 |
|
supxrmnf2 |
|- ( A C_ RR* -> sup ( ( A \ { -oo } ) , RR* , < ) = sup ( A , RR* , < ) ) |
33 |
1 32
|
syl |
|- ( ph -> sup ( ( A \ { -oo } ) , RR* , < ) = sup ( A , RR* , < ) ) |
34 |
33
|
eqcomd |
|- ( ph -> sup ( A , RR* , < ) = sup ( ( A \ { -oo } ) , RR* , < ) ) |
35 |
34
|
adantr |
|- ( ( ph /\ -. +oo e. A ) -> sup ( A , RR* , < ) = sup ( ( A \ { -oo } ) , RR* , < ) ) |
36 |
|
rexr |
|- ( y e. RR -> y e. RR* ) |
37 |
36
|
adantr |
|- ( ( y e. RR /\ -u y e. ( A \ { -oo } ) ) -> y e. RR* ) |
38 |
|
simpl |
|- ( ( y e. RR /\ -u y e. ( A \ { -oo } ) ) -> y e. RR ) |
39 |
38
|
rexnegd |
|- ( ( y e. RR /\ -u y e. ( A \ { -oo } ) ) -> -e y = -u y ) |
40 |
|
eldifi |
|- ( -u y e. ( A \ { -oo } ) -> -u y e. A ) |
41 |
40
|
adantl |
|- ( ( y e. RR /\ -u y e. ( A \ { -oo } ) ) -> -u y e. A ) |
42 |
39 41
|
eqeltrd |
|- ( ( y e. RR /\ -u y e. ( A \ { -oo } ) ) -> -e y e. A ) |
43 |
37 42
|
jca |
|- ( ( y e. RR /\ -u y e. ( A \ { -oo } ) ) -> ( y e. RR* /\ -e y e. A ) ) |
44 |
|
rabid |
|- ( y e. { y e. RR* | -e y e. A } <-> ( y e. RR* /\ -e y e. A ) ) |
45 |
43 44
|
sylibr |
|- ( ( y e. RR /\ -u y e. ( A \ { -oo } ) ) -> y e. { y e. RR* | -e y e. A } ) |
46 |
|
renepnf |
|- ( y e. RR -> y =/= +oo ) |
47 |
|
elsni |
|- ( y e. { +oo } -> y = +oo ) |
48 |
47
|
necon3ai |
|- ( y =/= +oo -> -. y e. { +oo } ) |
49 |
46 48
|
syl |
|- ( y e. RR -> -. y e. { +oo } ) |
50 |
38 49
|
syl |
|- ( ( y e. RR /\ -u y e. ( A \ { -oo } ) ) -> -. y e. { +oo } ) |
51 |
45 50
|
eldifd |
|- ( ( y e. RR /\ -u y e. ( A \ { -oo } ) ) -> y e. ( { y e. RR* | -e y e. A } \ { +oo } ) ) |
52 |
51
|
ex |
|- ( y e. RR -> ( -u y e. ( A \ { -oo } ) -> y e. ( { y e. RR* | -e y e. A } \ { +oo } ) ) ) |
53 |
52
|
rgen |
|- A. y e. RR ( -u y e. ( A \ { -oo } ) -> y e. ( { y e. RR* | -e y e. A } \ { +oo } ) ) |
54 |
53
|
a1i |
|- ( -. +oo e. A -> A. y e. RR ( -u y e. ( A \ { -oo } ) -> y e. ( { y e. RR* | -e y e. A } \ { +oo } ) ) ) |
55 |
|
nfrab1 |
|- F/_ y { y e. RR* | -e y e. A } |
56 |
|
nfcv |
|- F/_ y { +oo } |
57 |
55 56
|
nfdif |
|- F/_ y ( { y e. RR* | -e y e. A } \ { +oo } ) |
58 |
57
|
rabssf |
|- ( { y e. RR | -u y e. ( A \ { -oo } ) } C_ ( { y e. RR* | -e y e. A } \ { +oo } ) <-> A. y e. RR ( -u y e. ( A \ { -oo } ) -> y e. ( { y e. RR* | -e y e. A } \ { +oo } ) ) ) |
59 |
54 58
|
sylibr |
|- ( -. +oo e. A -> { y e. RR | -u y e. ( A \ { -oo } ) } C_ ( { y e. RR* | -e y e. A } \ { +oo } ) ) |
60 |
|
nfv |
|- F/ y -. +oo e. A |
61 |
|
nfcv |
|- F/_ y RR |
62 |
|
eldifi |
|- ( y e. ( { y e. RR* | -e y e. A } \ { +oo } ) -> y e. { y e. RR* | -e y e. A } ) |
63 |
7 62
|
sseldi |
|- ( y e. ( { y e. RR* | -e y e. A } \ { +oo } ) -> y e. RR* ) |
64 |
63
|
adantl |
|- ( ( -. +oo e. A /\ y e. ( { y e. RR* | -e y e. A } \ { +oo } ) ) -> y e. RR* ) |
65 |
44
|
simprbi |
|- ( y e. { y e. RR* | -e y e. A } -> -e y e. A ) |
66 |
62 65
|
syl |
|- ( y e. ( { y e. RR* | -e y e. A } \ { +oo } ) -> -e y e. A ) |
67 |
12
|
biimpac |
|- ( ( -e y e. A /\ y = -oo ) -> +oo e. A ) |
68 |
67
|
adantll |
|- ( ( ( -. +oo e. A /\ -e y e. A ) /\ y = -oo ) -> +oo e. A ) |
69 |
|
simpll |
|- ( ( ( -. +oo e. A /\ -e y e. A ) /\ y = -oo ) -> -. +oo e. A ) |
70 |
68 69
|
pm2.65da |
|- ( ( -. +oo e. A /\ -e y e. A ) -> -. y = -oo ) |
71 |
70
|
neqned |
|- ( ( -. +oo e. A /\ -e y e. A ) -> y =/= -oo ) |
72 |
66 71
|
sylan2 |
|- ( ( -. +oo e. A /\ y e. ( { y e. RR* | -e y e. A } \ { +oo } ) ) -> y =/= -oo ) |
73 |
|
eldifsni |
|- ( y e. ( { y e. RR* | -e y e. A } \ { +oo } ) -> y =/= +oo ) |
74 |
73
|
adantl |
|- ( ( -. +oo e. A /\ y e. ( { y e. RR* | -e y e. A } \ { +oo } ) ) -> y =/= +oo ) |
75 |
64 72 74
|
xrred |
|- ( ( -. +oo e. A /\ y e. ( { y e. RR* | -e y e. A } \ { +oo } ) ) -> y e. RR ) |
76 |
60 57 61 75
|
ssdf2 |
|- ( -. +oo e. A -> ( { y e. RR* | -e y e. A } \ { +oo } ) C_ RR ) |
77 |
75
|
rexnegd |
|- ( ( -. +oo e. A /\ y e. ( { y e. RR* | -e y e. A } \ { +oo } ) ) -> -e y = -u y ) |
78 |
66
|
adantl |
|- ( ( -. +oo e. A /\ y e. ( { y e. RR* | -e y e. A } \ { +oo } ) ) -> -e y e. A ) |
79 |
63
|
adantr |
|- ( ( y e. ( { y e. RR* | -e y e. A } \ { +oo } ) /\ -e y e. { -oo } ) -> y e. RR* ) |
80 |
|
elsni |
|- ( -e y e. { -oo } -> -e y = -oo ) |
81 |
80
|
adantl |
|- ( ( y e. ( { y e. RR* | -e y e. A } \ { +oo } ) /\ -e y e. { -oo } ) -> -e y = -oo ) |
82 |
|
xnegeq |
|- ( -e y = -oo -> -e -e y = -e -oo ) |
83 |
2
|
a1i |
|- ( -e y = -oo -> -e -oo = +oo ) |
84 |
82 83
|
eqtr2d |
|- ( -e y = -oo -> +oo = -e -e y ) |
85 |
84
|
adantl |
|- ( ( y e. RR* /\ -e y = -oo ) -> +oo = -e -e y ) |
86 |
|
xnegneg |
|- ( y e. RR* -> -e -e y = y ) |
87 |
86
|
adantr |
|- ( ( y e. RR* /\ -e y = -oo ) -> -e -e y = y ) |
88 |
85 87
|
eqtr2d |
|- ( ( y e. RR* /\ -e y = -oo ) -> y = +oo ) |
89 |
79 81 88
|
syl2anc |
|- ( ( y e. ( { y e. RR* | -e y e. A } \ { +oo } ) /\ -e y e. { -oo } ) -> y = +oo ) |
90 |
73
|
neneqd |
|- ( y e. ( { y e. RR* | -e y e. A } \ { +oo } ) -> -. y = +oo ) |
91 |
90
|
adantr |
|- ( ( y e. ( { y e. RR* | -e y e. A } \ { +oo } ) /\ -e y e. { -oo } ) -> -. y = +oo ) |
92 |
89 91
|
pm2.65da |
|- ( y e. ( { y e. RR* | -e y e. A } \ { +oo } ) -> -. -e y e. { -oo } ) |
93 |
92
|
adantl |
|- ( ( -. +oo e. A /\ y e. ( { y e. RR* | -e y e. A } \ { +oo } ) ) -> -. -e y e. { -oo } ) |
94 |
78 93
|
eldifd |
|- ( ( -. +oo e. A /\ y e. ( { y e. RR* | -e y e. A } \ { +oo } ) ) -> -e y e. ( A \ { -oo } ) ) |
95 |
77 94
|
eqeltrrd |
|- ( ( -. +oo e. A /\ y e. ( { y e. RR* | -e y e. A } \ { +oo } ) ) -> -u y e. ( A \ { -oo } ) ) |
96 |
95
|
ralrimiva |
|- ( -. +oo e. A -> A. y e. ( { y e. RR* | -e y e. A } \ { +oo } ) -u y e. ( A \ { -oo } ) ) |
97 |
76 96
|
jca |
|- ( -. +oo e. A -> ( ( { y e. RR* | -e y e. A } \ { +oo } ) C_ RR /\ A. y e. ( { y e. RR* | -e y e. A } \ { +oo } ) -u y e. ( A \ { -oo } ) ) ) |
98 |
57 61
|
ssrabf |
|- ( ( { y e. RR* | -e y e. A } \ { +oo } ) C_ { y e. RR | -u y e. ( A \ { -oo } ) } <-> ( ( { y e. RR* | -e y e. A } \ { +oo } ) C_ RR /\ A. y e. ( { y e. RR* | -e y e. A } \ { +oo } ) -u y e. ( A \ { -oo } ) ) ) |
99 |
97 98
|
sylibr |
|- ( -. +oo e. A -> ( { y e. RR* | -e y e. A } \ { +oo } ) C_ { y e. RR | -u y e. ( A \ { -oo } ) } ) |
100 |
59 99
|
eqssd |
|- ( -. +oo e. A -> { y e. RR | -u y e. ( A \ { -oo } ) } = ( { y e. RR* | -e y e. A } \ { +oo } ) ) |
101 |
100
|
infeq1d |
|- ( -. +oo e. A -> inf ( { y e. RR | -u y e. ( A \ { -oo } ) } , RR* , < ) = inf ( ( { y e. RR* | -e y e. A } \ { +oo } ) , RR* , < ) ) |
102 |
|
infxrpnf2 |
|- ( { y e. RR* | -e y e. A } C_ RR* -> inf ( ( { y e. RR* | -e y e. A } \ { +oo } ) , RR* , < ) = inf ( { y e. RR* | -e y e. A } , RR* , < ) ) |
103 |
7 102
|
ax-mp |
|- inf ( ( { y e. RR* | -e y e. A } \ { +oo } ) , RR* , < ) = inf ( { y e. RR* | -e y e. A } , RR* , < ) |
104 |
103
|
a1i |
|- ( -. +oo e. A -> inf ( ( { y e. RR* | -e y e. A } \ { +oo } ) , RR* , < ) = inf ( { y e. RR* | -e y e. A } , RR* , < ) ) |
105 |
101 104
|
eqtr2d |
|- ( -. +oo e. A -> inf ( { y e. RR* | -e y e. A } , RR* , < ) = inf ( { y e. RR | -u y e. ( A \ { -oo } ) } , RR* , < ) ) |
106 |
105
|
xnegeqd |
|- ( -. +oo e. A -> -e inf ( { y e. RR* | -e y e. A } , RR* , < ) = -e inf ( { y e. RR | -u y e. ( A \ { -oo } ) } , RR* , < ) ) |
107 |
106
|
adantl |
|- ( ( ph /\ -. +oo e. A ) -> -e inf ( { y e. RR* | -e y e. A } , RR* , < ) = -e inf ( { y e. RR | -u y e. ( A \ { -oo } ) } , RR* , < ) ) |
108 |
31 35 107
|
3eqtr4d |
|- ( ( ph /\ -. +oo e. A ) -> sup ( A , RR* , < ) = -e inf ( { y e. RR* | -e y e. A } , RR* , < ) ) |
109 |
21 108
|
pm2.61dan |
|- ( ph -> sup ( A , RR* , < ) = -e inf ( { y e. RR* | -e y e. A } , RR* , < ) ) |
110 |
|
xnegeq |
|- ( y = x -> -e y = -e x ) |
111 |
110
|
eleq1d |
|- ( y = x -> ( -e y e. A <-> -e x e. A ) ) |
112 |
111
|
cbvrabv |
|- { y e. RR* | -e y e. A } = { x e. RR* | -e x e. A } |
113 |
112
|
infeq1i |
|- inf ( { y e. RR* | -e y e. A } , RR* , < ) = inf ( { x e. RR* | -e x e. A } , RR* , < ) |
114 |
113
|
xnegeqi |
|- -e inf ( { y e. RR* | -e y e. A } , RR* , < ) = -e inf ( { x e. RR* | -e x e. A } , RR* , < ) |
115 |
114
|
a1i |
|- ( ph -> -e inf ( { y e. RR* | -e y e. A } , RR* , < ) = -e inf ( { x e. RR* | -e x e. A } , RR* , < ) ) |
116 |
109 115
|
eqtrd |
|- ( ph -> sup ( A , RR* , < ) = -e inf ( { x e. RR* | -e x e. A } , RR* , < ) ) |