Metamath Proof Explorer

Theorem supxrge

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 supxrge.xph 
|- F/ x ph
supxrge.a 
|- ( ph -> A C_ RR* )
supxrge.b 
|- ( ph -> B e. RR* )
supxrge.y 
|- ( ( ph /\ x e. RR+ ) -> E. y e. A B <_ ( y +e x ) )
Assertion supxrge 
|- ( ph -> B <_ sup ( A , RR* , < ) )

Proof

Step Hyp Ref Expression
1 supxrge.xph 
 |-  F/ x ph
2 supxrge.a 
 |-  ( ph -> A C_ RR* )
3 supxrge.b 
 |-  ( ph -> B e. RR* )
4 supxrge.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 /\ +oo e. A ) -> B <_ +oo )
8 2 adantr 
 |-  ( ( ph /\ +oo e. A ) -> A C_ RR* )
9 simpr 
 |-  ( ( ph /\ +oo e. A ) -> +oo e. A )
10 supxrpnf 
 |-  ( ( A C_ RR* /\ +oo e. A ) -> sup ( A , RR* , < ) = +oo )
11 8 9 10 syl2anc 
 |-  ( ( ph /\ +oo e. A ) -> sup ( A , RR* , < ) = +oo )
12 11 eqcomd 
 |-  ( ( ph /\ +oo e. A ) -> +oo = sup ( A , RR* , < ) )
13 7 12 breqtrd 
 |-  ( ( ph /\ +oo e. A ) -> B <_ sup ( A , RR* , < ) )
14 simpr 
 |-  ( ( ph /\ B = -oo ) -> B = -oo )
15 supxrcl 
 |-  ( A C_ RR* -> sup ( A , RR* , < ) e. RR* )
16 2 15 syl 
 |-  ( ph -> sup ( A , RR* , < ) e. RR* )
17 mnfle 
 |-  ( sup ( A , RR* , < ) e. RR* -> -oo <_ sup ( A , RR* , < ) )
18 16 17 syl 
 |-  ( ph -> -oo <_ sup ( A , RR* , < ) )
19 18 adantr 
 |-  ( ( ph /\ B = -oo ) -> -oo <_ sup ( A , RR* , < ) )
20 14 19 eqbrtrd 
 |-  ( ( ph /\ B = -oo ) -> B <_ sup ( A , RR* , < ) )
21 20 adantlr 
 |-  ( ( ( ph /\ -. +oo e. A ) /\ B = -oo ) -> B <_ sup ( A , RR* , < ) )
22 simpl 
 |-  ( ( ( ph /\ -. +oo e. A ) /\ -. B = -oo ) -> ( ph /\ -. +oo e. A ) )
23 neqne 
 |-  ( -. B = -oo -> B =/= -oo )
24 23 adantl 
 |-  ( ( ( ph /\ -. +oo e. A ) /\ -. B = -oo ) -> B =/= -oo )
25 nfv 
 |-  F/ w ( ( ph /\ -. +oo e. A ) /\ B =/= -oo )
26 2 adantr 
 |-  ( ( ph /\ -. +oo e. A ) -> A C_ RR* )
27 26 adantr 
 |-  ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) -> A C_ RR* )
28 3 adantr 
 |-  ( ( ph /\ -. +oo e. A ) -> B e. RR* )
29 28 adantr 
 |-  ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) -> B e. RR* )
30 simpl 
 |-  ( ( ph /\ w e. RR+ ) -> ph )
31 rphalfcl 
 |-  ( w e. RR+ -> ( w / 2 ) e. RR+ )
32 31 adantl 
 |-  ( ( ph /\ w e. RR+ ) -> ( w / 2 ) e. RR+ )
33 ovex 
 |-  ( w / 2 ) e. _V
34 nfcv 
 |-  F/_ x ( w / 2 )
35 nfv 
 |-  F/ x ( w / 2 ) e. RR+
36 1 35 nfan 
 |-  F/ x ( ph /\ ( w / 2 ) e. RR+ )
37 nfv 
 |-  F/ x E. y e. A B <_ ( y +e ( w / 2 ) )
38 36 37 nfim 
 |-  F/ x ( ( ph /\ ( w / 2 ) e. RR+ ) -> E. y e. A B <_ ( y +e ( w / 2 ) ) )
39 eleq1 
 |-  ( x = ( w / 2 ) -> ( x e. RR+ <-> ( w / 2 ) e. RR+ ) )
40 39 anbi2d 
 |-  ( x = ( w / 2 ) -> ( ( ph /\ x e. RR+ ) <-> ( ph /\ ( w / 2 ) e. RR+ ) ) )
41 oveq2 
 |-  ( x = ( w / 2 ) -> ( y +e x ) = ( y +e ( w / 2 ) ) )
42 41 breq2d 
 |-  ( x = ( w / 2 ) -> ( B <_ ( y +e x ) <-> B <_ ( y +e ( w / 2 ) ) ) )
43 42 rexbidv 
 |-  ( x = ( w / 2 ) -> ( E. y e. A B <_ ( y +e x ) <-> E. y e. A B <_ ( y +e ( w / 2 ) ) ) )
44 40 43 imbi12d 
 |-  ( x = ( w / 2 ) -> ( ( ( ph /\ x e. RR+ ) -> E. y e. A B <_ ( y +e x ) ) <-> ( ( ph /\ ( w / 2 ) e. RR+ ) -> E. y e. A B <_ ( y +e ( w / 2 ) ) ) ) )
45 34 38 44 4 vtoclgf 
 |-  ( ( w / 2 ) e. _V -> ( ( ph /\ ( w / 2 ) e. RR+ ) -> E. y e. A B <_ ( y +e ( w / 2 ) ) ) )
46 33 45 ax-mp 
 |-  ( ( ph /\ ( w / 2 ) e. RR+ ) -> E. y e. A B <_ ( y +e ( w / 2 ) ) )
47 30 32 46 syl2anc 
 |-  ( ( ph /\ w e. RR+ ) -> E. y e. A B <_ ( y +e ( w / 2 ) ) )
48 47 adantlr 
 |-  ( ( ( ph /\ -. +oo e. A ) /\ w e. RR+ ) -> E. y e. A B <_ ( y +e ( w / 2 ) ) )
49 48 adantlr 
 |-  ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) -> E. y e. A B <_ ( y +e ( w / 2 ) ) )
50 nfv 
 |-  F/ y ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ )
51 neneq 
 |-  ( B =/= -oo -> -. B = -oo )
52 51 adantl 
 |-  ( ( ph /\ B =/= -oo ) -> -. B = -oo )
53 3 adantr 
 |-  ( ( ph /\ B =/= -oo ) -> B e. RR* )
54 ngtmnft 
 |-  ( B e. RR* -> ( B = -oo <-> -. -oo < B ) )
55 53 54 syl 
 |-  ( ( ph /\ B =/= -oo ) -> ( B = -oo <-> -. -oo < B ) )
56 52 55 mtbid 
 |-  ( ( ph /\ B =/= -oo ) -> -. -. -oo < B )
57 56 notnotrd 
 |-  ( ( ph /\ B =/= -oo ) -> -oo < B )
58 57 ad4ant13 
 |-  ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) -> -oo < B )
59 58 3ad2ant1 
 |-  ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) -> -oo < B )
60 29 adantr 
 |-  ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) -> B e. RR* )
61 60 3ad2ant1 
 |-  ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) -> B e. RR* )
62 61 adantr 
 |-  ( ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) /\ -. -oo < y ) -> B e. RR* )
63 mnfxr 
 |-  -oo e. RR*
64 63 a1i 
 |-  ( ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) /\ -. -oo < y ) -> -oo e. RR* )
65 simpl3 
 |-  ( ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) /\ -. -oo < y ) -> B <_ ( y +e ( w / 2 ) ) )
66 simpr 
 |-  ( ( ( ph /\ y e. A ) /\ -. -oo < y ) -> -. -oo < y )
67 2 sselda 
 |-  ( ( ph /\ y e. A ) -> y e. RR* )
68 67 adantr 
 |-  ( ( ( ph /\ y e. A ) /\ -. -oo < y ) -> y e. RR* )
69 ngtmnft 
 |-  ( y e. RR* -> ( y = -oo <-> -. -oo < y ) )
70 68 69 syl 
 |-  ( ( ( ph /\ y e. A ) /\ -. -oo < y ) -> ( y = -oo <-> -. -oo < y ) )
71 66 70 mpbird 
 |-  ( ( ( ph /\ y e. A ) /\ -. -oo < y ) -> y = -oo )
72 71 oveq1d 
 |-  ( ( ( ph /\ y e. A ) /\ -. -oo < y ) -> ( y +e ( w / 2 ) ) = ( -oo +e ( w / 2 ) ) )
73 72 adantllr 
 |-  ( ( ( ( ph /\ w e. RR+ ) /\ y e. A ) /\ -. -oo < y ) -> ( y +e ( w / 2 ) ) = ( -oo +e ( w / 2 ) ) )
74 31 rpxrd 
 |-  ( w e. RR+ -> ( w / 2 ) e. RR* )
75 31 rpred 
 |-  ( w e. RR+ -> ( w / 2 ) e. RR )
76 renepnf 
 |-  ( ( w / 2 ) e. RR -> ( w / 2 ) =/= +oo )
77 75 76 syl 
 |-  ( w e. RR+ -> ( w / 2 ) =/= +oo )
78 xaddmnf2 
 |-  ( ( ( w / 2 ) e. RR* /\ ( w / 2 ) =/= +oo ) -> ( -oo +e ( w / 2 ) ) = -oo )
79 74 77 78 syl2anc 
 |-  ( w e. RR+ -> ( -oo +e ( w / 2 ) ) = -oo )
80 79 adantl 
 |-  ( ( ph /\ w e. RR+ ) -> ( -oo +e ( w / 2 ) ) = -oo )
81 80 ad2antrr 
 |-  ( ( ( ( ph /\ w e. RR+ ) /\ y e. A ) /\ -. -oo < y ) -> ( -oo +e ( w / 2 ) ) = -oo )
82 73 81 eqtrd 
 |-  ( ( ( ( ph /\ w e. RR+ ) /\ y e. A ) /\ -. -oo < y ) -> ( y +e ( w / 2 ) ) = -oo )
83 82 adantl3r 
 |-  ( ( ( ( ( ph /\ -. +oo e. A ) /\ w e. RR+ ) /\ y e. A ) /\ -. -oo < y ) -> ( y +e ( w / 2 ) ) = -oo )
84 83 adantl3r 
 |-  ( ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A ) /\ -. -oo < y ) -> ( y +e ( w / 2 ) ) = -oo )
85 84 3adantl3 
 |-  ( ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) /\ -. -oo < y ) -> ( y +e ( w / 2 ) ) = -oo )
86 65 85 breqtrd 
 |-  ( ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) /\ -. -oo < y ) -> B <_ -oo )
87 mnfle 
 |-  ( B e. RR* -> -oo <_ B )
88 3 87 syl 
 |-  ( ph -> -oo <_ B )
89 88 adantr 
 |-  ( ( ph /\ -. +oo e. A ) -> -oo <_ B )
90 89 ad3antrrr 
 |-  ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ -. -oo < y ) -> -oo <_ B )
91 90 3ad2antl1 
 |-  ( ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) /\ -. -oo < y ) -> -oo <_ B )
92 62 64 86 91 xrletrid 
 |-  ( ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) /\ -. -oo < y ) -> B = -oo )
93 simpllr 
 |-  ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ -. -oo < y ) -> B =/= -oo )
94 93 3ad2antl1 
 |-  ( ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) /\ -. -oo < y ) -> B =/= -oo )
95 94 neneqd 
 |-  ( ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) /\ -. -oo < y ) -> -. B = -oo )
96 92 95 condan 
 |-  ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) -> -oo < y )
97 simpr 
 |-  ( ( ( ph /\ y e. A ) /\ -. y < +oo ) -> -. y < +oo )
98 67 adantr 
 |-  ( ( ( ph /\ y e. A ) /\ -. y < +oo ) -> y e. RR* )
99 nltpnft 
 |-  ( y e. RR* -> ( y = +oo <-> -. y < +oo ) )
100 98 99 syl 
 |-  ( ( ( ph /\ y e. A ) /\ -. y < +oo ) -> ( y = +oo <-> -. y < +oo ) )
101 97 100 mpbird 
 |-  ( ( ( ph /\ y e. A ) /\ -. y < +oo ) -> y = +oo )
102 101 eqcomd 
 |-  ( ( ( ph /\ y e. A ) /\ -. y < +oo ) -> +oo = y )
103 simpr 
 |-  ( ( ph /\ y e. A ) -> y e. A )
104 103 adantr 
 |-  ( ( ( ph /\ y e. A ) /\ -. y < +oo ) -> y e. A )
105 102 104 eqeltrd 
 |-  ( ( ( ph /\ y e. A ) /\ -. y < +oo ) -> +oo e. A )
106 105 3adantl2 
 |-  ( ( ( ph /\ -. +oo e. A /\ y e. A ) /\ -. y < +oo ) -> +oo e. A )
107 simpl2 
 |-  ( ( ( ph /\ -. +oo e. A /\ y e. A ) /\ -. y < +oo ) -> -. +oo e. A )
108 106 107 condan 
 |-  ( ( ph /\ -. +oo e. A /\ y e. A ) -> y < +oo )
109 108 ad5ant125 
 |-  ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A ) -> y < +oo )
110 109 3adant3 
 |-  ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) -> y < +oo )
111 96 110 jca 
 |-  ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) -> ( -oo < y /\ y < +oo ) )
112 67 ad5ant15 
 |-  ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A ) -> y e. RR* )
113 112 3adant3 
 |-  ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) -> y e. RR* )
114 xrrebnd 
 |-  ( y e. RR* -> ( y e. RR <-> ( -oo < y /\ y < +oo ) ) )
115 113 114 syl 
 |-  ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) -> ( y e. RR <-> ( -oo < y /\ y < +oo ) ) )
116 111 115 mpbird 
 |-  ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) -> y e. RR )
117 75 adantl 
 |-  ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) -> ( w / 2 ) e. RR )
118 117 3ad2ant1 
 |-  ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) -> ( w / 2 ) e. RR )
119 rexadd 
 |-  ( ( y e. RR /\ ( w / 2 ) e. RR ) -> ( y +e ( w / 2 ) ) = ( y + ( w / 2 ) ) )
120 116 118 119 syl2anc 
 |-  ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) -> ( y +e ( w / 2 ) ) = ( y + ( w / 2 ) ) )
121 116 118 readdcld 
 |-  ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) -> ( y + ( w / 2 ) ) e. RR )
122 120 121 eqeltrd 
 |-  ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) -> ( y +e ( w / 2 ) ) e. RR )
123 122 rexrd 
 |-  ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) -> ( y +e ( w / 2 ) ) e. RR* )
124 pnfxr 
 |-  +oo e. RR*
125 124 a1i 
 |-  ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) -> +oo e. RR* )
126 simp3 
 |-  ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) -> B <_ ( y +e ( w / 2 ) ) )
127 122 ltpnfd 
 |-  ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) -> ( y +e ( w / 2 ) ) < +oo )
128 61 123 125 126 127 xrlelttrd 
 |-  ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) -> B < +oo )
129 59 128 jca 
 |-  ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) -> ( -oo < B /\ B < +oo ) )
130 xrrebnd 
 |-  ( B e. RR* -> ( B e. RR <-> ( -oo < B /\ B < +oo ) ) )
131 61 130 syl 
 |-  ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) -> ( B e. RR <-> ( -oo < B /\ B < +oo ) ) )
132 129 131 mpbird 
 |-  ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) -> B e. RR )
133 rpre 
 |-  ( w e. RR+ -> w e. RR )
134 133 adantl 
 |-  ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) -> w e. RR )
135 134 3ad2ant1 
 |-  ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) -> w e. RR )
136 rexadd 
 |-  ( ( y e. RR /\ w e. RR ) -> ( y +e w ) = ( y + w ) )
137 116 135 136 syl2anc 
 |-  ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) -> ( y +e w ) = ( y + w ) )
138 116 135 readdcld 
 |-  ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) -> ( y + w ) e. RR )
139 137 138 eqeltrd 
 |-  ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) -> ( y +e w ) e. RR )
140 rphalflt 
 |-  ( w e. RR+ -> ( w / 2 ) < w )
141 140 adantl 
 |-  ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) -> ( w / 2 ) < w )
142 141 3ad2ant1 
 |-  ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) -> ( w / 2 ) < w )
143 118 135 116 142 ltadd2dd 
 |-  ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) -> ( y + ( w / 2 ) ) < ( y + w ) )
144 120 137 breq12d 
 |-  ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) -> ( ( y +e ( w / 2 ) ) < ( y +e w ) <-> ( y + ( w / 2 ) ) < ( y + w ) ) )
145 143 144 mpbird 
 |-  ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) -> ( y +e ( w / 2 ) ) < ( y +e w ) )
146 132 122 139 126 145 lelttrd 
 |-  ( ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) /\ y e. A /\ B <_ ( y +e ( w / 2 ) ) ) -> B < ( y +e w ) )
147 146 3exp 
 |-  ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) -> ( y e. A -> ( B <_ ( y +e ( w / 2 ) ) -> B < ( y +e w ) ) ) )
148 50 147 reximdai 
 |-  ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) -> ( E. y e. A B <_ ( y +e ( w / 2 ) ) -> E. y e. A B < ( y +e w ) ) )
149 49 148 mpd 
 |-  ( ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) /\ w e. RR+ ) -> E. y e. A B < ( y +e w ) )
150 25 27 29 149 supxrgelem 
 |-  ( ( ( ph /\ -. +oo e. A ) /\ B =/= -oo ) -> B <_ sup ( A , RR* , < ) )
151 22 24 150 syl2anc 
 |-  ( ( ( ph /\ -. +oo e. A ) /\ -. B = -oo ) -> B <_ sup ( A , RR* , < ) )
152 21 151 pm2.61dan 
 |-  ( ( ph /\ -. +oo e. A ) -> B <_ sup ( A , RR* , < ) )
153 13 152 pm2.61dan 
 |-  ( ph -> B <_ sup ( A , RR* , < ) )