Metamath Proof Explorer

Theorem supxrgelem

Description: If an extended real number can be approximated from below by members of a set, then it is less than or equal to the supremum of the set. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses supxrgelem.xph 
|- F/ x ph
supxrgelem.a 
|- ( ph -> A C_ RR* )
supxrgelem.b 
|- ( ph -> B e. RR* )
supxrgelem.y 
|- ( ( ph /\ x e. RR+ ) -> E. y e. A B < ( y +e x ) )
Assertion supxrgelem 
|- ( ph -> B <_ sup ( A , RR* , < ) )

Proof

Step Hyp Ref Expression
1 supxrgelem.xph 
 |-  F/ x ph
2 supxrgelem.a 
 |-  ( ph -> A C_ RR* )
3 supxrgelem.b 
 |-  ( ph -> B e. RR* )
4 supxrgelem.y 
 |-  ( ( ph /\ x e. RR+ ) -> E. y e. A B < ( y +e x ) )
5 pnfge 
 |-  ( B e. RR* -> B <_ +oo )
6 3 5 syl 
 |-  ( ph -> B <_ +oo )
7 6 adantr 
 |-  ( ( ph /\ sup ( A , RR* , < ) = +oo ) -> B <_ +oo )
8 id 
 |-  ( sup ( A , RR* , < ) = +oo -> sup ( A , RR* , < ) = +oo )
9 8 eqcomd 
 |-  ( sup ( A , RR* , < ) = +oo -> +oo = sup ( A , RR* , < ) )
10 9 adantl 
 |-  ( ( ph /\ sup ( A , RR* , < ) = +oo ) -> +oo = sup ( A , RR* , < ) )
11 7 10 breqtrd 
 |-  ( ( ph /\ sup ( A , RR* , < ) = +oo ) -> B <_ sup ( A , RR* , < ) )
12 simpl 
 |-  ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) -> ph )
13 1rp 
 |-  1 e. RR+
14 nfcv 
 |-  F/_ x 1
15 nfv 
 |-  F/ x 1 e. RR+
16 1 15 nfan 
 |-  F/ x ( ph /\ 1 e. RR+ )
17 nfv 
 |-  F/ x E. y e. A B < ( y +e 1 )
18 16 17 nfim 
 |-  F/ x ( ( ph /\ 1 e. RR+ ) -> E. y e. A B < ( y +e 1 ) )
19 eleq1 
 |-  ( x = 1 -> ( x e. RR+ <-> 1 e. RR+ ) )
20 19 anbi2d 
 |-  ( x = 1 -> ( ( ph /\ x e. RR+ ) <-> ( ph /\ 1 e. RR+ ) ) )
21 oveq2 
 |-  ( x = 1 -> ( y +e x ) = ( y +e 1 ) )
22 21 breq2d 
 |-  ( x = 1 -> ( B < ( y +e x ) <-> B < ( y +e 1 ) ) )
23 22 rexbidv 
 |-  ( x = 1 -> ( E. y e. A B < ( y +e x ) <-> E. y e. A B < ( y +e 1 ) ) )
24 20 23 imbi12d 
 |-  ( x = 1 -> ( ( ( ph /\ x e. RR+ ) -> E. y e. A B < ( y +e x ) ) <-> ( ( ph /\ 1 e. RR+ ) -> E. y e. A B < ( y +e 1 ) ) ) )
25 14 18 24 4 vtoclgf 
 |-  ( 1 e. RR+ -> ( ( ph /\ 1 e. RR+ ) -> E. y e. A B < ( y +e 1 ) ) )
26 13 25 ax-mp 
 |-  ( ( ph /\ 1 e. RR+ ) -> E. y e. A B < ( y +e 1 ) )
27 13 26 mpan2 
 |-  ( ph -> E. y e. A B < ( y +e 1 ) )
28 27 adantr 
 |-  ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) -> E. y e. A B < ( y +e 1 ) )
29 mnfxr 
 |-  -oo e. RR*
30 29 a1i 
 |-  ( ( ph /\ y e. A /\ B < ( y +e 1 ) ) -> -oo e. RR* )
31 2 sselda 
 |-  ( ( ph /\ y e. A ) -> y e. RR* )
32 31 3adant3 
 |-  ( ( ph /\ y e. A /\ B < ( y +e 1 ) ) -> y e. RR* )
33 supxrcl 
 |-  ( A C_ RR* -> sup ( A , RR* , < ) e. RR* )
34 2 33 syl 
 |-  ( ph -> sup ( A , RR* , < ) e. RR* )
35 34 3ad2ant1 
 |-  ( ( ph /\ y e. A /\ B < ( y +e 1 ) ) -> sup ( A , RR* , < ) e. RR* )
36 simpl3 
 |-  ( ( ( ph /\ y e. A /\ B < ( y +e 1 ) ) /\ -. -oo < y ) -> B < ( y +e 1 ) )
37 simpr 
 |-  ( ( ( ph /\ y e. A ) /\ -. -oo < y ) -> -. -oo < y )
38 31 adantr 
 |-  ( ( ( ph /\ y e. A ) /\ -. -oo < y ) -> y e. RR* )
39 ngtmnft 
 |-  ( y e. RR* -> ( y = -oo <-> -. -oo < y ) )
40 38 39 syl 
 |-  ( ( ( ph /\ y e. A ) /\ -. -oo < y ) -> ( y = -oo <-> -. -oo < y ) )
41 37 40 mpbird 
 |-  ( ( ( ph /\ y e. A ) /\ -. -oo < y ) -> y = -oo )
42 41 oveq1d 
 |-  ( ( ( ph /\ y e. A ) /\ -. -oo < y ) -> ( y +e 1 ) = ( -oo +e 1 ) )
43 1xr 
 |-  1 e. RR*
44 43 a1i 
 |-  ( ( ( ph /\ y e. A ) /\ -. -oo < y ) -> 1 e. RR* )
45 1re 
 |-  1 e. RR
46 renepnf 
 |-  ( 1 e. RR -> 1 =/= +oo )
47 45 46 ax-mp 
 |-  1 =/= +oo
48 47 a1i 
 |-  ( ( ( ph /\ y e. A ) /\ -. -oo < y ) -> 1 =/= +oo )
49 xaddmnf2 
 |-  ( ( 1 e. RR* /\ 1 =/= +oo ) -> ( -oo +e 1 ) = -oo )
50 44 48 49 syl2anc 
 |-  ( ( ( ph /\ y e. A ) /\ -. -oo < y ) -> ( -oo +e 1 ) = -oo )
51 42 50 eqtrd 
 |-  ( ( ( ph /\ y e. A ) /\ -. -oo < y ) -> ( y +e 1 ) = -oo )
52 51 3adantl3 
 |-  ( ( ( ph /\ y e. A /\ B < ( y +e 1 ) ) /\ -. -oo < y ) -> ( y +e 1 ) = -oo )
53 36 52 breqtrd 
 |-  ( ( ( ph /\ y e. A /\ B < ( y +e 1 ) ) /\ -. -oo < y ) -> B < -oo )
54 nltmnf 
 |-  ( B e. RR* -> -. B < -oo )
55 3 54 syl 
 |-  ( ph -> -. B < -oo )
56 55 adantr 
 |-  ( ( ph /\ -. -oo < y ) -> -. B < -oo )
57 56 3ad2antl1 
 |-  ( ( ( ph /\ y e. A /\ B < ( y +e 1 ) ) /\ -. -oo < y ) -> -. B < -oo )
58 53 57 condan 
 |-  ( ( ph /\ y e. A /\ B < ( y +e 1 ) ) -> -oo < y )
59 2 adantr 
 |-  ( ( ph /\ y e. A ) -> A C_ RR* )
60 simpr 
 |-  ( ( ph /\ y e. A ) -> y e. A )
61 supxrub 
 |-  ( ( A C_ RR* /\ y e. A ) -> y <_ sup ( A , RR* , < ) )
62 59 60 61 syl2anc 
 |-  ( ( ph /\ y e. A ) -> y <_ sup ( A , RR* , < ) )
63 62 3adant3 
 |-  ( ( ph /\ y e. A /\ B < ( y +e 1 ) ) -> y <_ sup ( A , RR* , < ) )
64 30 32 35 58 63 xrltletrd 
 |-  ( ( ph /\ y e. A /\ B < ( y +e 1 ) ) -> -oo < sup ( A , RR* , < ) )
65 64 3exp 
 |-  ( ph -> ( y e. A -> ( B < ( y +e 1 ) -> -oo < sup ( A , RR* , < ) ) ) )
66 65 adantr 
 |-  ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) -> ( y e. A -> ( B < ( y +e 1 ) -> -oo < sup ( A , RR* , < ) ) ) )
67 66 rexlimdv 
 |-  ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) -> ( E. y e. A B < ( y +e 1 ) -> -oo < sup ( A , RR* , < ) ) )
68 28 67 mpd 
 |-  ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) -> -oo < sup ( A , RR* , < ) )
69 simpr 
 |-  ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) -> -. sup ( A , RR* , < ) = +oo )
70 nltpnft 
 |-  ( sup ( A , RR* , < ) e. RR* -> ( sup ( A , RR* , < ) = +oo <-> -. sup ( A , RR* , < ) < +oo ) )
71 34 70 syl 
 |-  ( ph -> ( sup ( A , RR* , < ) = +oo <-> -. sup ( A , RR* , < ) < +oo ) )
72 71 adantr 
 |-  ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) -> ( sup ( A , RR* , < ) = +oo <-> -. sup ( A , RR* , < ) < +oo ) )
73 69 72 mtbid 
 |-  ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) -> -. -. sup ( A , RR* , < ) < +oo )
74 73 notnotrd 
 |-  ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) -> sup ( A , RR* , < ) < +oo )
75 68 74 jca 
 |-  ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) -> ( -oo < sup ( A , RR* , < ) /\ sup ( A , RR* , < ) < +oo ) )
76 34 adantr 
 |-  ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) -> sup ( A , RR* , < ) e. RR* )
77 xrrebnd 
 |-  ( sup ( A , RR* , < ) e. RR* -> ( sup ( A , RR* , < ) e. RR <-> ( -oo < sup ( A , RR* , < ) /\ sup ( A , RR* , < ) < +oo ) ) )
78 76 77 syl 
 |-  ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) -> ( sup ( A , RR* , < ) e. RR <-> ( -oo < sup ( A , RR* , < ) /\ sup ( A , RR* , < ) < +oo ) ) )
79 75 78 mpbird 
 |-  ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) -> sup ( A , RR* , < ) e. RR )
80 simpl 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ -. B <_ sup ( A , RR* , < ) ) -> ( ph /\ sup ( A , RR* , < ) e. RR ) )
81 simpr 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ -. B <_ sup ( A , RR* , < ) ) -> -. B <_ sup ( A , RR* , < ) )
82 34 adantr 
 |-  ( ( ph /\ -. B <_ sup ( A , RR* , < ) ) -> sup ( A , RR* , < ) e. RR* )
83 3 adantr 
 |-  ( ( ph /\ -. B <_ sup ( A , RR* , < ) ) -> B e. RR* )
84 xrltnle 
 |-  ( ( sup ( A , RR* , < ) e. RR* /\ B e. RR* ) -> ( sup ( A , RR* , < ) < B <-> -. B <_ sup ( A , RR* , < ) ) )
85 82 83 84 syl2anc 
 |-  ( ( ph /\ -. B <_ sup ( A , RR* , < ) ) -> ( sup ( A , RR* , < ) < B <-> -. B <_ sup ( A , RR* , < ) ) )
86 85 adantlr 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ -. B <_ sup ( A , RR* , < ) ) -> ( sup ( A , RR* , < ) < B <-> -. B <_ sup ( A , RR* , < ) ) )
87 81 86 mpbird 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ -. B <_ sup ( A , RR* , < ) ) -> sup ( A , RR* , < ) < B )
88 simpll 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> ph )
89 29 a1i 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> -oo e. RR* )
90 88 34 syl 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> sup ( A , RR* , < ) e. RR* )
91 88 3 syl 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> B e. RR* )
92 mnfle 
 |-  ( sup ( A , RR* , < ) e. RR* -> -oo <_ sup ( A , RR* , < ) )
93 34 92 syl 
 |-  ( ph -> -oo <_ sup ( A , RR* , < ) )
94 93 ad2antrr 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> -oo <_ sup ( A , RR* , < ) )
95 simpr 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> sup ( A , RR* , < ) < B )
96 89 90 91 94 95 xrlelttrd 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> -oo < B )
97 id 
 |-  ( ph -> ph )
98 13 a1i 
 |-  ( ph -> 1 e. RR+ )
99 97 98 26 syl2anc 
 |-  ( ph -> E. y e. A B < ( y +e 1 ) )
100 99 ad2antrr 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> E. y e. A B < ( y +e 1 ) )
101 3 3ad2ant1 
 |-  ( ( ph /\ y e. A /\ B < ( y +e 1 ) ) -> B e. RR* )
102 43 a1i 
 |-  ( ( ph /\ y e. A /\ B < ( y +e 1 ) ) -> 1 e. RR* )
103 32 102 jca 
 |-  ( ( ph /\ y e. A /\ B < ( y +e 1 ) ) -> ( y e. RR* /\ 1 e. RR* ) )
104 xaddcl 
 |-  ( ( y e. RR* /\ 1 e. RR* ) -> ( y +e 1 ) e. RR* )
105 103 104 syl 
 |-  ( ( ph /\ y e. A /\ B < ( y +e 1 ) ) -> ( y +e 1 ) e. RR* )
106 pnfxr 
 |-  +oo e. RR*
107 106 a1i 
 |-  ( ( ph /\ y e. A /\ B < ( y +e 1 ) ) -> +oo e. RR* )
108 simp3 
 |-  ( ( ph /\ y e. A /\ B < ( y +e 1 ) ) -> B < ( y +e 1 ) )
109 31 43 104 sylancl 
 |-  ( ( ph /\ y e. A ) -> ( y +e 1 ) e. RR* )
110 pnfge 
 |-  ( ( y +e 1 ) e. RR* -> ( y +e 1 ) <_ +oo )
111 109 110 syl 
 |-  ( ( ph /\ y e. A ) -> ( y +e 1 ) <_ +oo )
112 111 3adant3 
 |-  ( ( ph /\ y e. A /\ B < ( y +e 1 ) ) -> ( y +e 1 ) <_ +oo )
113 101 105 107 108 112 xrltletrd 
 |-  ( ( ph /\ y e. A /\ B < ( y +e 1 ) ) -> B < +oo )
114 113 3exp 
 |-  ( ph -> ( y e. A -> ( B < ( y +e 1 ) -> B < +oo ) ) )
115 114 rexlimdv 
 |-  ( ph -> ( E. y e. A B < ( y +e 1 ) -> B < +oo ) )
116 88 115 syl 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> ( E. y e. A B < ( y +e 1 ) -> B < +oo ) )
117 100 116 mpd 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> B < +oo )
118 96 117 jca 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> ( -oo < B /\ B < +oo ) )
119 xrrebnd 
 |-  ( B e. RR* -> ( B e. RR <-> ( -oo < B /\ B < +oo ) ) )
120 91 119 syl 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> ( B e. RR <-> ( -oo < B /\ B < +oo ) ) )
121 118 120 mpbird 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> B e. RR )
122 simpr 
 |-  ( ( ph /\ sup ( A , RR* , < ) e. RR ) -> sup ( A , RR* , < ) e. RR )
123 122 adantr 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> sup ( A , RR* , < ) e. RR )
124 121 123 resubcld 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> ( B - sup ( A , RR* , < ) ) e. RR )
125 27 115 mpd 
 |-  ( ph -> B < +oo )
126 125 ad2antrr 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> B < +oo )
127 96 126 jca 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> ( -oo < B /\ B < +oo ) )
128 127 120 mpbird 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> B e. RR )
129 123 128 posdifd 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> ( sup ( A , RR* , < ) < B <-> 0 < ( B - sup ( A , RR* , < ) ) ) )
130 95 129 mpbid 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> 0 < ( B - sup ( A , RR* , < ) ) )
131 124 130 elrpd 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> ( B - sup ( A , RR* , < ) ) e. RR+ )
132 ovex 
 |-  ( B - sup ( A , RR* , < ) ) e. _V
133 nfcv 
 |-  F/_ x ( B - sup ( A , RR* , < ) )
134 nfv 
 |-  F/ x ( B - sup ( A , RR* , < ) ) e. RR+
135 1 134 nfan 
 |-  F/ x ( ph /\ ( B - sup ( A , RR* , < ) ) e. RR+ )
136 nfv 
 |-  F/ x E. y e. A B < ( y +e ( B - sup ( A , RR* , < ) ) )
137 135 136 nfim 
 |-  F/ x ( ( ph /\ ( B - sup ( A , RR* , < ) ) e. RR+ ) -> E. y e. A B < ( y +e ( B - sup ( A , RR* , < ) ) ) )
138 eleq1 
 |-  ( x = ( B - sup ( A , RR* , < ) ) -> ( x e. RR+ <-> ( B - sup ( A , RR* , < ) ) e. RR+ ) )
139 138 anbi2d 
 |-  ( x = ( B - sup ( A , RR* , < ) ) -> ( ( ph /\ x e. RR+ ) <-> ( ph /\ ( B - sup ( A , RR* , < ) ) e. RR+ ) ) )
140 oveq2 
 |-  ( x = ( B - sup ( A , RR* , < ) ) -> ( y +e x ) = ( y +e ( B - sup ( A , RR* , < ) ) ) )
141 140 breq2d 
 |-  ( x = ( B - sup ( A , RR* , < ) ) -> ( B < ( y +e x ) <-> B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) )
142 141 rexbidv 
 |-  ( x = ( B - sup ( A , RR* , < ) ) -> ( E. y e. A B < ( y +e x ) <-> E. y e. A B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) )
143 139 142 imbi12d 
 |-  ( x = ( B - sup ( A , RR* , < ) ) -> ( ( ( ph /\ x e. RR+ ) -> E. y e. A B < ( y +e x ) ) <-> ( ( ph /\ ( B - sup ( A , RR* , < ) ) e. RR+ ) -> E. y e. A B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) ) )
144 133 137 143 4 vtoclgf 
 |-  ( ( B - sup ( A , RR* , < ) ) e. _V -> ( ( ph /\ ( B - sup ( A , RR* , < ) ) e. RR+ ) -> E. y e. A B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) )
145 132 144 ax-mp 
 |-  ( ( ph /\ ( B - sup ( A , RR* , < ) ) e. RR+ ) -> E. y e. A B < ( y +e ( B - sup ( A , RR* , < ) ) ) )
146 88 131 145 syl2anc 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> E. y e. A B < ( y +e ( B - sup ( A , RR* , < ) ) ) )
147 ltpnf 
 |-  ( sup ( A , RR* , < ) e. RR -> sup ( A , RR* , < ) < +oo )
148 147 adantr 
 |-  ( ( sup ( A , RR* , < ) e. RR /\ y = +oo ) -> sup ( A , RR* , < ) < +oo )
149 id 
 |-  ( y = +oo -> y = +oo )
150 149 eqcomd 
 |-  ( y = +oo -> +oo = y )
151 150 adantl 
 |-  ( ( sup ( A , RR* , < ) e. RR /\ y = +oo ) -> +oo = y )
152 148 151 breqtrd 
 |-  ( ( sup ( A , RR* , < ) e. RR /\ y = +oo ) -> sup ( A , RR* , < ) < y )
153 152 adantll 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ y = +oo ) -> sup ( A , RR* , < ) < y )
154 153 ad5ant15 
 |-  ( ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. A ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) /\ y = +oo ) -> sup ( A , RR* , < ) < y )
155 simplll 
 |-  ( ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. A ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) /\ -. y = +oo ) -> ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) )
156 simpl 
 |-  ( ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. A ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) /\ -. -oo < y ) -> ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. A ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) )
157 88 41 sylanl1 
 |-  ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. A ) /\ -. -oo < y ) -> y = -oo )
158 157 adantlr 
 |-  ( ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. A ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) /\ -. -oo < y ) -> y = -oo )
159 simplr 
 |-  ( ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. A ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) /\ y = -oo ) -> B < ( y +e ( B - sup ( A , RR* , < ) ) ) )
160 oveq1 
 |-  ( y = -oo -> ( y +e ( B - sup ( A , RR* , < ) ) ) = ( -oo +e ( B - sup ( A , RR* , < ) ) ) )
161 160 adantl 
 |-  ( ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. A ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) /\ y = -oo ) -> ( y +e ( B - sup ( A , RR* , < ) ) ) = ( -oo +e ( B - sup ( A , RR* , < ) ) ) )
162 128 123 resubcld 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> ( B - sup ( A , RR* , < ) ) e. RR )
163 162 rexrd 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> ( B - sup ( A , RR* , < ) ) e. RR* )
164 163 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. A ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) /\ y = -oo ) -> ( B - sup ( A , RR* , < ) ) e. RR* )
165 renepnf 
 |-  ( ( B - sup ( A , RR* , < ) ) e. RR -> ( B - sup ( A , RR* , < ) ) =/= +oo )
166 124 165 syl 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> ( B - sup ( A , RR* , < ) ) =/= +oo )
167 166 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. A ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) /\ y = -oo ) -> ( B - sup ( A , RR* , < ) ) =/= +oo )
168 xaddmnf2 
 |-  ( ( ( B - sup ( A , RR* , < ) ) e. RR* /\ ( B - sup ( A , RR* , < ) ) =/= +oo ) -> ( -oo +e ( B - sup ( A , RR* , < ) ) ) = -oo )
169 164 167 168 syl2anc 
 |-  ( ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. A ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) /\ y = -oo ) -> ( -oo +e ( B - sup ( A , RR* , < ) ) ) = -oo )
170 161 169 eqtrd 
 |-  ( ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. A ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) /\ y = -oo ) -> ( y +e ( B - sup ( A , RR* , < ) ) ) = -oo )
171 159 170 breqtrd 
 |-  ( ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. A ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) /\ y = -oo ) -> B < -oo )
172 156 158 171 syl2anc 
 |-  ( ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. A ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) /\ -. -oo < y ) -> B < -oo )
173 55 ad5antr 
 |-  ( ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. A ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) /\ -. -oo < y ) -> -. B < -oo )
174 172 173 condan 
 |-  ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. A ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) -> -oo < y )
175 174 adantr 
 |-  ( ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. A ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) /\ -. y = +oo ) -> -oo < y )
176 simp3 
 |-  ( ( ph /\ y e. A /\ -. y = +oo ) -> -. y = +oo )
177 31 3adant3 
 |-  ( ( ph /\ y e. A /\ -. y = +oo ) -> y e. RR* )
178 nltpnft 
 |-  ( y e. RR* -> ( y = +oo <-> -. y < +oo ) )
179 177 178 syl 
 |-  ( ( ph /\ y e. A /\ -. y = +oo ) -> ( y = +oo <-> -. y < +oo ) )
180 176 179 mtbid 
 |-  ( ( ph /\ y e. A /\ -. y = +oo ) -> -. -. y < +oo )
181 180 notnotrd 
 |-  ( ( ph /\ y e. A /\ -. y = +oo ) -> y < +oo )
182 181 3adant1r 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ y e. A /\ -. y = +oo ) -> y < +oo )
183 182 ad5ant135 
 |-  ( ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. A ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) /\ -. y = +oo ) -> y < +oo )
184 175 183 jca 
 |-  ( ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. A ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) /\ -. y = +oo ) -> ( -oo < y /\ y < +oo ) )
185 31 adantlr 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ y e. A ) -> y e. RR* )
186 185 ad5ant13 
 |-  ( ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. A ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) /\ -. y = +oo ) -> y e. RR* )
187 xrrebnd 
 |-  ( y e. RR* -> ( y e. RR <-> ( -oo < y /\ y < +oo ) ) )
188 186 187 syl 
 |-  ( ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. A ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) /\ -. y = +oo ) -> ( y e. RR <-> ( -oo < y /\ y < +oo ) ) )
189 184 188 mpbird 
 |-  ( ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. A ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) /\ -. y = +oo ) -> y e. RR )
190 simplr 
 |-  ( ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. A ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) /\ -. y = +oo ) -> B < ( y +e ( B - sup ( A , RR* , < ) ) ) )
191 121 ad2antrr 
 |-  ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. RR ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) -> B e. RR )
192 simpr 
 |-  ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. RR ) -> y e. RR )
193 124 adantr 
 |-  ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. RR ) -> ( B - sup ( A , RR* , < ) ) e. RR )
194 rexadd 
 |-  ( ( y e. RR /\ ( B - sup ( A , RR* , < ) ) e. RR ) -> ( y +e ( B - sup ( A , RR* , < ) ) ) = ( y + ( B - sup ( A , RR* , < ) ) ) )
195 192 193 194 syl2anc 
 |-  ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. RR ) -> ( y +e ( B - sup ( A , RR* , < ) ) ) = ( y + ( B - sup ( A , RR* , < ) ) ) )
196 192 193 readdcld 
 |-  ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. RR ) -> ( y + ( B - sup ( A , RR* , < ) ) ) e. RR )
197 195 196 eqeltrd 
 |-  ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. RR ) -> ( y +e ( B - sup ( A , RR* , < ) ) ) e. RR )
198 197 adantr 
 |-  ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. RR ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) -> ( y +e ( B - sup ( A , RR* , < ) ) ) e. RR )
199 simpr 
 |-  ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. RR ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) -> B < ( y +e ( B - sup ( A , RR* , < ) ) ) )
200 191 198 191 199 ltsub1dd 
 |-  ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. RR ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) -> ( B - B ) < ( ( y +e ( B - sup ( A , RR* , < ) ) ) - B ) )
201 121 recnd 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> B e. CC )
202 201 subidd 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> ( B - B ) = 0 )
203 202 ad2antrr 
 |-  ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. RR ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) -> ( B - B ) = 0 )
204 201 adantr 
 |-  ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. RR ) -> B e. CC )
205 192 recnd 
 |-  ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. RR ) -> y e. CC )
206 122 recnd 
 |-  ( ( ph /\ sup ( A , RR* , < ) e. RR ) -> sup ( A , RR* , < ) e. CC )
207 206 ad2antrr 
 |-  ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. RR ) -> sup ( A , RR* , < ) e. CC )
208 205 207 subcld 
 |-  ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. RR ) -> ( y - sup ( A , RR* , < ) ) e. CC )
209 205 204 207 addsub12d 
 |-  ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. RR ) -> ( y + ( B - sup ( A , RR* , < ) ) ) = ( B + ( y - sup ( A , RR* , < ) ) ) )
210 195 209 eqtrd 
 |-  ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. RR ) -> ( y +e ( B - sup ( A , RR* , < ) ) ) = ( B + ( y - sup ( A , RR* , < ) ) ) )
211 204 208 210 mvrladdd 
 |-  ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. RR ) -> ( ( y +e ( B - sup ( A , RR* , < ) ) ) - B ) = ( y - sup ( A , RR* , < ) ) )
212 211 adantr 
 |-  ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. RR ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) -> ( ( y +e ( B - sup ( A , RR* , < ) ) ) - B ) = ( y - sup ( A , RR* , < ) ) )
213 203 212 breq12d 
 |-  ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. RR ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) -> ( ( B - B ) < ( ( y +e ( B - sup ( A , RR* , < ) ) ) - B ) <-> 0 < ( y - sup ( A , RR* , < ) ) ) )
214 200 213 mpbid 
 |-  ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. RR ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) -> 0 < ( y - sup ( A , RR* , < ) ) )
215 123 ad2antrr 
 |-  ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. RR ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) -> sup ( A , RR* , < ) e. RR )
216 simplr 
 |-  ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. RR ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) -> y e. RR )
217 215 216 posdifd 
 |-  ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. RR ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) -> ( sup ( A , RR* , < ) < y <-> 0 < ( y - sup ( A , RR* , < ) ) ) )
218 214 217 mpbird 
 |-  ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. RR ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) -> sup ( A , RR* , < ) < y )
219 155 189 190 218 syl21anc 
 |-  ( ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. A ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) /\ -. y = +oo ) -> sup ( A , RR* , < ) < y )
220 154 219 pm2.61dan 
 |-  ( ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. A ) /\ B < ( y +e ( B - sup ( A , RR* , < ) ) ) ) -> sup ( A , RR* , < ) < y )
221 220 ex 
 |-  ( ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) /\ y e. A ) -> ( B < ( y +e ( B - sup ( A , RR* , < ) ) ) -> sup ( A , RR* , < ) < y ) )
222 221 reximdva 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> ( E. y e. A B < ( y +e ( B - sup ( A , RR* , < ) ) ) -> E. y e. A sup ( A , RR* , < ) < y ) )
223 146 222 mpd 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ sup ( A , RR* , < ) < B ) -> E. y e. A sup ( A , RR* , < ) < y )
224 80 87 223 syl2anc 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ -. B <_ sup ( A , RR* , < ) ) -> E. y e. A sup ( A , RR* , < ) < y )
225 59 33 syl 
 |-  ( ( ph /\ y e. A ) -> sup ( A , RR* , < ) e. RR* )
226 31 225 xrlenltd 
 |-  ( ( ph /\ y e. A ) -> ( y <_ sup ( A , RR* , < ) <-> -. sup ( A , RR* , < ) < y ) )
227 62 226 mpbid 
 |-  ( ( ph /\ y e. A ) -> -. sup ( A , RR* , < ) < y )
228 227 ralrimiva 
 |-  ( ph -> A. y e. A -. sup ( A , RR* , < ) < y )
229 ralnex 
 |-  ( A. y e. A -. sup ( A , RR* , < ) < y <-> -. E. y e. A sup ( A , RR* , < ) < y )
230 228 229 sylib 
 |-  ( ph -> -. E. y e. A sup ( A , RR* , < ) < y )
231 230 ad2antrr 
 |-  ( ( ( ph /\ sup ( A , RR* , < ) e. RR ) /\ -. B <_ sup ( A , RR* , < ) ) -> -. E. y e. A sup ( A , RR* , < ) < y )
232 224 231 condan 
 |-  ( ( ph /\ sup ( A , RR* , < ) e. RR ) -> B <_ sup ( A , RR* , < ) )
233 12 79 232 syl2anc 
 |-  ( ( ph /\ -. sup ( A , RR* , < ) = +oo ) -> B <_ sup ( A , RR* , < ) )
234 11 233 pm2.61dan 
 |-  ( ph -> B <_ sup ( A , RR* , < ) )