Metamath Proof Explorer

Theorem ioodvbdlimc2lem

Description: Limit at the upper bound of an open interval, for a function with bounded derivative. (Contributed by Glauco Siliprandi, 11-Dec-2019) (Revised by AV, 3-Oct-2020)

Ref Expression
Hypotheses ioodvbdlimc2lem.a 
|- ( ph -> A e. RR )
ioodvbdlimc2lem.b 
|- ( ph -> B e. RR )
ioodvbdlimc2lem.altb 
|- ( ph -> A < B )
ioodvbdlimc2lem.f 
|- ( ph -> F : ( A (,) B ) --> RR )
ioodvbdlimc2lem.dmdv 
|- ( ph -> dom ( RR _D F ) = ( A (,) B ) )
ioodvbdlimc2lem.dvbd 
|- ( ph -> E. y e. RR A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ y )
ioodvbdlimc2lem.y 
|- Y = sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < )
ioodvbdlimc2lem.m 
|- M = ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 )
ioodvbdlimc2lem.s 
|- S = ( j e. ( ZZ>= ` M ) |-> ( F ` ( B - ( 1 / j ) ) ) )
ioodvbdlimc2lem.r 
|- R = ( j e. ( ZZ>= ` M ) |-> ( B - ( 1 / j ) ) )
ioodvbdlimc2lem.n 
|- N = if ( M <_ ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , M )
ioodvbdlimc2lem.ch 
|- ( ch <-> ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( z - B ) ) < ( 1 / j ) ) )
Assertion ioodvbdlimc2lem 
|- ( ph -> ( limsup ` S ) e. ( F limCC B ) )

Proof

Step Hyp Ref Expression
1 ioodvbdlimc2lem.a 
 |-  ( ph -> A e. RR )
2 ioodvbdlimc2lem.b 
 |-  ( ph -> B e. RR )
3 ioodvbdlimc2lem.altb 
 |-  ( ph -> A < B )
4 ioodvbdlimc2lem.f 
 |-  ( ph -> F : ( A (,) B ) --> RR )
5 ioodvbdlimc2lem.dmdv 
 |-  ( ph -> dom ( RR _D F ) = ( A (,) B ) )
6 ioodvbdlimc2lem.dvbd 
 |-  ( ph -> E. y e. RR A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ y )
7 ioodvbdlimc2lem.y 
 |-  Y = sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < )
8 ioodvbdlimc2lem.m 
 |-  M = ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 )
9 ioodvbdlimc2lem.s 
 |-  S = ( j e. ( ZZ>= ` M ) |-> ( F ` ( B - ( 1 / j ) ) ) )
10 ioodvbdlimc2lem.r 
 |-  R = ( j e. ( ZZ>= ` M ) |-> ( B - ( 1 / j ) ) )
11 ioodvbdlimc2lem.n 
 |-  N = if ( M <_ ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , M )
12 ioodvbdlimc2lem.ch 
 |-  ( ch <-> ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( z - B ) ) < ( 1 / j ) ) )
13 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
14 zssre 
 |-  ZZ C_ RR
15 13 14 sstri 
 |-  ( ZZ>= ` M ) C_ RR
16 15 a1i 
 |-  ( ph -> ( ZZ>= ` M ) C_ RR )
17 2 1 resubcld 
 |-  ( ph -> ( B - A ) e. RR )
18 1 2 posdifd 
 |-  ( ph -> ( A < B <-> 0 < ( B - A ) ) )
19 3 18 mpbid 
 |-  ( ph -> 0 < ( B - A ) )
20 19 gt0ne0d 
 |-  ( ph -> ( B - A ) =/= 0 )
21 17 20 rereccld 
 |-  ( ph -> ( 1 / ( B - A ) ) e. RR )
22 0red 
 |-  ( ph -> 0 e. RR )
23 17 19 recgt0d 
 |-  ( ph -> 0 < ( 1 / ( B - A ) ) )
24 22 21 23 ltled 
 |-  ( ph -> 0 <_ ( 1 / ( B - A ) ) )
25 flge0nn0 
 |-  ( ( ( 1 / ( B - A ) ) e. RR /\ 0 <_ ( 1 / ( B - A ) ) ) -> ( |_ ` ( 1 / ( B - A ) ) ) e. NN0 )
26 21 24 25 syl2anc 
 |-  ( ph -> ( |_ ` ( 1 / ( B - A ) ) ) e. NN0 )
27 peano2nn0 
 |-  ( ( |_ ` ( 1 / ( B - A ) ) ) e. NN0 -> ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) e. NN0 )
28 26 27 syl 
 |-  ( ph -> ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) e. NN0 )
29 8 28 eqeltrid 
 |-  ( ph -> M e. NN0 )
30 29 nn0zd 
 |-  ( ph -> M e. ZZ )
31 eqid 
 |-  ( ZZ>= ` M ) = ( ZZ>= ` M )
32 31 uzsup 
 |-  ( M e. ZZ -> sup ( ( ZZ>= ` M ) , RR* , < ) = +oo )
33 30 32 syl 
 |-  ( ph -> sup ( ( ZZ>= ` M ) , RR* , < ) = +oo )
34 4 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> F : ( A (,) B ) --> RR )
35 1 rexrd 
 |-  ( ph -> A e. RR* )
36 35 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> A e. RR* )
37 2 rexrd 
 |-  ( ph -> B e. RR* )
38 37 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> B e. RR* )
39 2 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> B e. RR )
40 eluzelre 
 |-  ( j e. ( ZZ>= ` M ) -> j e. RR )
41 40 adantl 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> j e. RR )
42 0red 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> 0 e. RR )
43 0red 
 |-  ( j e. ( ZZ>= ` M ) -> 0 e. RR )
44 1red 
 |-  ( j e. ( ZZ>= ` M ) -> 1 e. RR )
45 43 44 readdcld 
 |-  ( j e. ( ZZ>= ` M ) -> ( 0 + 1 ) e. RR )
46 45 adantl 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( 0 + 1 ) e. RR )
47 43 ltp1d 
 |-  ( j e. ( ZZ>= ` M ) -> 0 < ( 0 + 1 ) )
48 47 adantl 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> 0 < ( 0 + 1 ) )
49 eluzel2 
 |-  ( j e. ( ZZ>= ` M ) -> M e. ZZ )
50 49 zred 
 |-  ( j e. ( ZZ>= ` M ) -> M e. RR )
51 50 adantl 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> M e. RR )
52 21 flcld 
 |-  ( ph -> ( |_ ` ( 1 / ( B - A ) ) ) e. ZZ )
53 52 zred 
 |-  ( ph -> ( |_ ` ( 1 / ( B - A ) ) ) e. RR )
54 1red 
 |-  ( ph -> 1 e. RR )
55 26 nn0ge0d 
 |-  ( ph -> 0 <_ ( |_ ` ( 1 / ( B - A ) ) ) )
56 22 53 54 55 leadd1dd 
 |-  ( ph -> ( 0 + 1 ) <_ ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) )
57 56 8 breqtrrdi 
 |-  ( ph -> ( 0 + 1 ) <_ M )
58 57 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( 0 + 1 ) <_ M )
59 eluzle 
 |-  ( j e. ( ZZ>= ` M ) -> M <_ j )
60 59 adantl 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> M <_ j )
61 46 51 41 58 60 letrd 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( 0 + 1 ) <_ j )
62 42 46 41 48 61 ltletrd 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> 0 < j )
63 62 gt0ne0d 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> j =/= 0 )
64 41 63 rereccld 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( 1 / j ) e. RR )
65 39 64 resubcld 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( B - ( 1 / j ) ) e. RR )
66 1 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> A e. RR )
67 29 nn0red 
 |-  ( ph -> M e. RR )
68 22 54 readdcld 
 |-  ( ph -> ( 0 + 1 ) e. RR )
69 53 54 readdcld 
 |-  ( ph -> ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) e. RR )
70 22 ltp1d 
 |-  ( ph -> 0 < ( 0 + 1 ) )
71 22 68 69 70 56 ltletrd 
 |-  ( ph -> 0 < ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) )
72 71 8 breqtrrdi 
 |-  ( ph -> 0 < M )
73 72 gt0ne0d 
 |-  ( ph -> M =/= 0 )
74 67 73 rereccld 
 |-  ( ph -> ( 1 / M ) e. RR )
75 74 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( 1 / M ) e. RR )
76 39 75 resubcld 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( B - ( 1 / M ) ) e. RR )
77 8 eqcomi 
 |-  ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) = M
78 77 oveq2i 
 |-  ( 1 / ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) ) = ( 1 / M )
79 78 74 eqeltrid 
 |-  ( ph -> ( 1 / ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) ) e. RR )
80 21 23 elrpd 
 |-  ( ph -> ( 1 / ( B - A ) ) e. RR+ )
81 69 71 elrpd 
 |-  ( ph -> ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) e. RR+ )
82 1rp 
 |-  1 e. RR+
83 82 a1i 
 |-  ( ph -> 1 e. RR+ )
84 fllelt 
 |-  ( ( 1 / ( B - A ) ) e. RR -> ( ( |_ ` ( 1 / ( B - A ) ) ) <_ ( 1 / ( B - A ) ) /\ ( 1 / ( B - A ) ) < ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) ) )
85 21 84 syl 
 |-  ( ph -> ( ( |_ ` ( 1 / ( B - A ) ) ) <_ ( 1 / ( B - A ) ) /\ ( 1 / ( B - A ) ) < ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) ) )
86 85 simprd 
 |-  ( ph -> ( 1 / ( B - A ) ) < ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) )
87 80 81 83 86 ltdiv2dd 
 |-  ( ph -> ( 1 / ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) ) < ( 1 / ( 1 / ( B - A ) ) ) )
88 17 recnd 
 |-  ( ph -> ( B - A ) e. CC )
89 88 20 recrecd 
 |-  ( ph -> ( 1 / ( 1 / ( B - A ) ) ) = ( B - A ) )
90 87 89 breqtrd 
 |-  ( ph -> ( 1 / ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) ) < ( B - A ) )
91 79 17 2 90 ltsub2dd 
 |-  ( ph -> ( B - ( B - A ) ) < ( B - ( 1 / ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) ) ) )
92 2 recnd 
 |-  ( ph -> B e. CC )
93 1 recnd 
 |-  ( ph -> A e. CC )
94 92 93 nncand 
 |-  ( ph -> ( B - ( B - A ) ) = A )
95 78 oveq2i 
 |-  ( B - ( 1 / ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) ) ) = ( B - ( 1 / M ) )
96 95 a1i 
 |-  ( ph -> ( B - ( 1 / ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) ) ) = ( B - ( 1 / M ) ) )
97 91 94 96 3brtr3d 
 |-  ( ph -> A < ( B - ( 1 / M ) ) )
98 97 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> A < ( B - ( 1 / M ) ) )
99 67 72 elrpd 
 |-  ( ph -> M e. RR+ )
100 99 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> M e. RR+ )
101 41 62 elrpd 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> j e. RR+ )
102 1red 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> 1 e. RR )
103 0le1 
 |-  0 <_ 1
104 103 a1i 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> 0 <_ 1 )
105 100 101 102 104 60 lediv2ad 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( 1 / j ) <_ ( 1 / M ) )
106 64 75 39 105 lesub2dd 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( B - ( 1 / M ) ) <_ ( B - ( 1 / j ) ) )
107 66 76 65 98 106 ltletrd 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> A < ( B - ( 1 / j ) ) )
108 101 rpreccld 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( 1 / j ) e. RR+ )
109 39 108 ltsubrpd 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( B - ( 1 / j ) ) < B )
110 36 38 65 107 109 eliood 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( B - ( 1 / j ) ) e. ( A (,) B ) )
111 34 110 ffvelrnd 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( F ` ( B - ( 1 / j ) ) ) e. RR )
112 111 9 fmptd 
 |-  ( ph -> S : ( ZZ>= ` M ) --> RR )
113 1 2 3 4 5 6 dvbdfbdioo 
 |-  ( ph -> E. b e. RR A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b )
114 67 adantr 
 |-  ( ( ph /\ A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b ) -> M e. RR )
115 simpr 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> j e. ( ZZ>= ` M ) )
116 9 fvmpt2 
 |-  ( ( j e. ( ZZ>= ` M ) /\ ( F ` ( B - ( 1 / j ) ) ) e. RR ) -> ( S ` j ) = ( F ` ( B - ( 1 / j ) ) ) )
117 115 111 116 syl2anc 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( S ` j ) = ( F ` ( B - ( 1 / j ) ) ) )
118 117 fveq2d 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( abs ` ( S ` j ) ) = ( abs ` ( F ` ( B - ( 1 / j ) ) ) ) )
119 118 adantlr 
 |-  ( ( ( ph /\ A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b ) /\ j e. ( ZZ>= ` M ) ) -> ( abs ` ( S ` j ) ) = ( abs ` ( F ` ( B - ( 1 / j ) ) ) ) )
120 simplr 
 |-  ( ( ( ph /\ A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b ) /\ j e. ( ZZ>= ` M ) ) -> A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b )
121 110 adantlr 
 |-  ( ( ( ph /\ A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b ) /\ j e. ( ZZ>= ` M ) ) -> ( B - ( 1 / j ) ) e. ( A (,) B ) )
122 2fveq3 
 |-  ( x = ( B - ( 1 / j ) ) -> ( abs ` ( F ` x ) ) = ( abs ` ( F ` ( B - ( 1 / j ) ) ) ) )
123 122 breq1d 
 |-  ( x = ( B - ( 1 / j ) ) -> ( ( abs ` ( F ` x ) ) <_ b <-> ( abs ` ( F ` ( B - ( 1 / j ) ) ) ) <_ b ) )
124 123 rspccva 
 |-  ( ( A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b /\ ( B - ( 1 / j ) ) e. ( A (,) B ) ) -> ( abs ` ( F ` ( B - ( 1 / j ) ) ) ) <_ b )
125 120 121 124 syl2anc 
 |-  ( ( ( ph /\ A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b ) /\ j e. ( ZZ>= ` M ) ) -> ( abs ` ( F ` ( B - ( 1 / j ) ) ) ) <_ b )
126 119 125 eqbrtrd 
 |-  ( ( ( ph /\ A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b ) /\ j e. ( ZZ>= ` M ) ) -> ( abs ` ( S ` j ) ) <_ b )
127 126 a1d 
 |-  ( ( ( ph /\ A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b ) /\ j e. ( ZZ>= ` M ) ) -> ( M <_ j -> ( abs ` ( S ` j ) ) <_ b ) )
128 127 ralrimiva 
 |-  ( ( ph /\ A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b ) -> A. j e. ( ZZ>= ` M ) ( M <_ j -> ( abs ` ( S ` j ) ) <_ b ) )
129 breq1 
 |-  ( k = M -> ( k <_ j <-> M <_ j ) )
130 129 imbi1d 
 |-  ( k = M -> ( ( k <_ j -> ( abs ` ( S ` j ) ) <_ b ) <-> ( M <_ j -> ( abs ` ( S ` j ) ) <_ b ) ) )
131 130 ralbidv 
 |-  ( k = M -> ( A. j e. ( ZZ>= ` M ) ( k <_ j -> ( abs ` ( S ` j ) ) <_ b ) <-> A. j e. ( ZZ>= ` M ) ( M <_ j -> ( abs ` ( S ` j ) ) <_ b ) ) )
132 131 rspcev 
 |-  ( ( M e. RR /\ A. j e. ( ZZ>= ` M ) ( M <_ j -> ( abs ` ( S ` j ) ) <_ b ) ) -> E. k e. RR A. j e. ( ZZ>= ` M ) ( k <_ j -> ( abs ` ( S ` j ) ) <_ b ) )
133 114 128 132 syl2anc 
 |-  ( ( ph /\ A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b ) -> E. k e. RR A. j e. ( ZZ>= ` M ) ( k <_ j -> ( abs ` ( S ` j ) ) <_ b ) )
134 133 ex 
 |-  ( ph -> ( A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b -> E. k e. RR A. j e. ( ZZ>= ` M ) ( k <_ j -> ( abs ` ( S ` j ) ) <_ b ) ) )
135 134 reximdv 
 |-  ( ph -> ( E. b e. RR A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b -> E. b e. RR E. k e. RR A. j e. ( ZZ>= ` M ) ( k <_ j -> ( abs ` ( S ` j ) ) <_ b ) ) )
136 113 135 mpd 
 |-  ( ph -> E. b e. RR E. k e. RR A. j e. ( ZZ>= ` M ) ( k <_ j -> ( abs ` ( S ` j ) ) <_ b ) )
137 16 33 112 136 limsupre 
 |-  ( ph -> ( limsup ` S ) e. RR )
138 137 recnd 
 |-  ( ph -> ( limsup ` S ) e. CC )
139 eluzelre 
 |-  ( j e. ( ZZ>= ` N ) -> j e. RR )
140 139 adantl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> j e. RR )
141 0red 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> 0 e. RR )
142 52 peano2zd 
 |-  ( ph -> ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) e. ZZ )
143 8 142 eqeltrid 
 |-  ( ph -> M e. ZZ )
144 143 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> M e. ZZ )
145 144 zred 
 |-  ( ( ph /\ x e. RR+ ) -> M e. RR )
146 145 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> M e. RR )
147 72 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> 0 < M )
148 ioomidp 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( ( A + B ) / 2 ) e. ( A (,) B ) )
149 1 2 3 148 syl3anc 
 |-  ( ph -> ( ( A + B ) / 2 ) e. ( A (,) B ) )
150 ne0i 
 |-  ( ( ( A + B ) / 2 ) e. ( A (,) B ) -> ( A (,) B ) =/= (/) )
151 149 150 syl 
 |-  ( ph -> ( A (,) B ) =/= (/) )
152 ioossre 
 |-  ( A (,) B ) C_ RR
153 152 a1i 
 |-  ( ph -> ( A (,) B ) C_ RR )
154 dvfre 
 |-  ( ( F : ( A (,) B ) --> RR /\ ( A (,) B ) C_ RR ) -> ( RR _D F ) : dom ( RR _D F ) --> RR )
155 4 153 154 syl2anc 
 |-  ( ph -> ( RR _D F ) : dom ( RR _D F ) --> RR )
156 5 feq2d 
 |-  ( ph -> ( ( RR _D F ) : dom ( RR _D F ) --> RR <-> ( RR _D F ) : ( A (,) B ) --> RR ) )
157 155 156 mpbid 
 |-  ( ph -> ( RR _D F ) : ( A (,) B ) --> RR )
158 157 ffvelrnda 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D F ) ` x ) e. RR )
159 158 recnd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D F ) ` x ) e. CC )
160 159 abscld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( abs ` ( ( RR _D F ) ` x ) ) e. RR )
161 eqid 
 |-  ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) = ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) )
162 eqid 
 |-  sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) = sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < )
163 151 160 6 161 162 suprnmpt 
 |-  ( ph -> ( sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) e. RR /\ A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) ) )
164 163 simpld 
 |-  ( ph -> sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) e. RR )
165 7 164 eqeltrid 
 |-  ( ph -> Y e. RR )
166 165 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> Y e. RR )
167 rpre 
 |-  ( x e. RR+ -> x e. RR )
168 167 rehalfcld 
 |-  ( x e. RR+ -> ( x / 2 ) e. RR )
169 168 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> ( x / 2 ) e. RR )
170 167 recnd 
 |-  ( x e. RR+ -> x e. CC )
171 170 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> x e. CC )
172 2cnd 
 |-  ( ( ph /\ x e. RR+ ) -> 2 e. CC )
173 rpne0 
 |-  ( x e. RR+ -> x =/= 0 )
174 173 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> x =/= 0 )
175 2ne0 
 |-  2 =/= 0
176 175 a1i 
 |-  ( ( ph /\ x e. RR+ ) -> 2 =/= 0 )
177 171 172 174 176 divne0d 
 |-  ( ( ph /\ x e. RR+ ) -> ( x / 2 ) =/= 0 )
178 166 169 177 redivcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( Y / ( x / 2 ) ) e. RR )
179 178 flcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( |_ ` ( Y / ( x / 2 ) ) ) e. ZZ )
180 179 peano2zd 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) e. ZZ )
181 180 144 ifcld 
 |-  ( ( ph /\ x e. RR+ ) -> if ( M <_ ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , M ) e. ZZ )
182 11 181 eqeltrid 
 |-  ( ( ph /\ x e. RR+ ) -> N e. ZZ )
183 182 zred 
 |-  ( ( ph /\ x e. RR+ ) -> N e. RR )
184 183 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> N e. RR )
185 180 zred 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) e. RR )
186 max1 
 |-  ( ( M e. RR /\ ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) e. RR ) -> M <_ if ( M <_ ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , M ) )
187 145 185 186 syl2anc 
 |-  ( ( ph /\ x e. RR+ ) -> M <_ if ( M <_ ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , M ) )
188 187 11 breqtrrdi 
 |-  ( ( ph /\ x e. RR+ ) -> M <_ N )
189 188 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> M <_ N )
190 eluzle 
 |-  ( j e. ( ZZ>= ` N ) -> N <_ j )
191 190 adantl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> N <_ j )
192 146 184 140 189 191 letrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> M <_ j )
193 141 146 140 147 192 ltletrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> 0 < j )
194 193 gt0ne0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> j =/= 0 )
195 140 194 rereccld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> ( 1 / j ) e. RR )
196 140 193 recgt0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> 0 < ( 1 / j ) )
197 195 196 elrpd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> ( 1 / j ) e. RR+ )
198 197 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) -> ( 1 / j ) e. RR+ )
199 12 biimpi 
 |-  ( ch -> ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( z - B ) ) < ( 1 / j ) ) )
200 simp-5l 
 |-  ( ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( z - B ) ) < ( 1 / j ) ) -> ph )
201 199 200 syl 
 |-  ( ch -> ph )
202 201 4 syl 
 |-  ( ch -> F : ( A (,) B ) --> RR )
203 199 simplrd 
 |-  ( ch -> z e. ( A (,) B ) )
204 202 203 ffvelrnd 
 |-  ( ch -> ( F ` z ) e. RR )
205 204 recnd 
 |-  ( ch -> ( F ` z ) e. CC )
206 201 112 syl 
 |-  ( ch -> S : ( ZZ>= ` M ) --> RR )
207 simp-5r 
 |-  ( ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( z - B ) ) < ( 1 / j ) ) -> x e. RR+ )
208 199 207 syl 
 |-  ( ch -> x e. RR+ )
209 eluz2 
 |-  ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) )
210 144 182 188 209 syl3anbrc 
 |-  ( ( ph /\ x e. RR+ ) -> N e. ( ZZ>= ` M ) )
211 201 208 210 syl2anc 
 |-  ( ch -> N e. ( ZZ>= ` M ) )
212 uzss 
 |-  ( N e. ( ZZ>= ` M ) -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) )
213 211 212 syl 
 |-  ( ch -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) )
214 simp-4r 
 |-  ( ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( z - B ) ) < ( 1 / j ) ) -> j e. ( ZZ>= ` N ) )
215 199 214 syl 
 |-  ( ch -> j e. ( ZZ>= ` N ) )
216 213 215 sseldd 
 |-  ( ch -> j e. ( ZZ>= ` M ) )
217 206 216 ffvelrnd 
 |-  ( ch -> ( S ` j ) e. RR )
218 217 recnd 
 |-  ( ch -> ( S ` j ) e. CC )
219 201 138 syl 
 |-  ( ch -> ( limsup ` S ) e. CC )
220 205 218 219 npncand 
 |-  ( ch -> ( ( ( F ` z ) - ( S ` j ) ) + ( ( S ` j ) - ( limsup ` S ) ) ) = ( ( F ` z ) - ( limsup ` S ) ) )
221 220 eqcomd 
 |-  ( ch -> ( ( F ` z ) - ( limsup ` S ) ) = ( ( ( F ` z ) - ( S ` j ) ) + ( ( S ` j ) - ( limsup ` S ) ) ) )
222 221 fveq2d 
 |-  ( ch -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) = ( abs ` ( ( ( F ` z ) - ( S ` j ) ) + ( ( S ` j ) - ( limsup ` S ) ) ) ) )
223 204 217 resubcld 
 |-  ( ch -> ( ( F ` z ) - ( S ` j ) ) e. RR )
224 201 137 syl 
 |-  ( ch -> ( limsup ` S ) e. RR )
225 217 224 resubcld 
 |-  ( ch -> ( ( S ` j ) - ( limsup ` S ) ) e. RR )
226 223 225 readdcld 
 |-  ( ch -> ( ( ( F ` z ) - ( S ` j ) ) + ( ( S ` j ) - ( limsup ` S ) ) ) e. RR )
227 226 recnd 
 |-  ( ch -> ( ( ( F ` z ) - ( S ` j ) ) + ( ( S ` j ) - ( limsup ` S ) ) ) e. CC )
228 227 abscld 
 |-  ( ch -> ( abs ` ( ( ( F ` z ) - ( S ` j ) ) + ( ( S ` j ) - ( limsup ` S ) ) ) ) e. RR )
229 223 recnd 
 |-  ( ch -> ( ( F ` z ) - ( S ` j ) ) e. CC )
230 229 abscld 
 |-  ( ch -> ( abs ` ( ( F ` z ) - ( S ` j ) ) ) e. RR )
231 225 recnd 
 |-  ( ch -> ( ( S ` j ) - ( limsup ` S ) ) e. CC )
232 231 abscld 
 |-  ( ch -> ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) e. RR )
233 230 232 readdcld 
 |-  ( ch -> ( ( abs ` ( ( F ` z ) - ( S ` j ) ) ) + ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) ) e. RR )
234 208 rpred 
 |-  ( ch -> x e. RR )
235 229 231 abstrid 
 |-  ( ch -> ( abs ` ( ( ( F ` z ) - ( S ` j ) ) + ( ( S ` j ) - ( limsup ` S ) ) ) ) <_ ( ( abs ` ( ( F ` z ) - ( S ` j ) ) ) + ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) ) )
236 234 rehalfcld 
 |-  ( ch -> ( x / 2 ) e. RR )
237 201 216 117 syl2anc 
 |-  ( ch -> ( S ` j ) = ( F ` ( B - ( 1 / j ) ) ) )
238 237 oveq2d 
 |-  ( ch -> ( ( F ` z ) - ( S ` j ) ) = ( ( F ` z ) - ( F ` ( B - ( 1 / j ) ) ) ) )
239 238 fveq2d 
 |-  ( ch -> ( abs ` ( ( F ` z ) - ( S ` j ) ) ) = ( abs ` ( ( F ` z ) - ( F ` ( B - ( 1 / j ) ) ) ) ) )
240 239 230 eqeltrrd 
 |-  ( ch -> ( abs ` ( ( F ` z ) - ( F ` ( B - ( 1 / j ) ) ) ) ) e. RR )
241 201 165 syl 
 |-  ( ch -> Y e. RR )
242 152 203 sselid 
 |-  ( ch -> z e. RR )
243 201 216 65 syl2anc 
 |-  ( ch -> ( B - ( 1 / j ) ) e. RR )
244 242 243 resubcld 
 |-  ( ch -> ( z - ( B - ( 1 / j ) ) ) e. RR )
245 241 244 remulcld 
 |-  ( ch -> ( Y x. ( z - ( B - ( 1 / j ) ) ) ) e. RR )
246 201 1 syl 
 |-  ( ch -> A e. RR )
247 201 2 syl 
 |-  ( ch -> B e. RR )
248 201 5 syl 
 |-  ( ch -> dom ( RR _D F ) = ( A (,) B ) )
249 163 simprd 
 |-  ( ph -> A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) )
250 7 breq2i 
 |-  ( ( abs ` ( ( RR _D F ) ` x ) ) <_ Y <-> ( abs ` ( ( RR _D F ) ` x ) ) <_ sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) )
251 250 ralbii 
 |-  ( A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ Y <-> A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) )
252 249 251 sylibr 
 |-  ( ph -> A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ Y )
253 201 252 syl 
 |-  ( ch -> A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ Y )
254 2fveq3 
 |-  ( w = x -> ( abs ` ( ( RR _D F ) ` w ) ) = ( abs ` ( ( RR _D F ) ` x ) ) )
255 254 breq1d 
 |-  ( w = x -> ( ( abs ` ( ( RR _D F ) ` w ) ) <_ Y <-> ( abs ` ( ( RR _D F ) ` x ) ) <_ Y ) )
256 255 cbvralvw 
 |-  ( A. w e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` w ) ) <_ Y <-> A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ Y )
257 253 256 sylibr 
 |-  ( ch -> A. w e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` w ) ) <_ Y )
258 201 216 110 syl2anc 
 |-  ( ch -> ( B - ( 1 / j ) ) e. ( A (,) B ) )
259 243 rexrd 
 |-  ( ch -> ( B - ( 1 / j ) ) e. RR* )
260 201 37 syl 
 |-  ( ch -> B e. RR* )
261 15 216 sselid 
 |-  ( ch -> j e. RR )
262 201 216 63 syl2anc 
 |-  ( ch -> j =/= 0 )
263 261 262 rereccld 
 |-  ( ch -> ( 1 / j ) e. RR )
264 247 242 resubcld 
 |-  ( ch -> ( B - z ) e. RR )
265 242 247 resubcld 
 |-  ( ch -> ( z - B ) e. RR )
266 265 recnd 
 |-  ( ch -> ( z - B ) e. CC )
267 266 abscld 
 |-  ( ch -> ( abs ` ( z - B ) ) e. RR )
268 264 leabsd 
 |-  ( ch -> ( B - z ) <_ ( abs ` ( B - z ) ) )
269 201 92 syl 
 |-  ( ch -> B e. CC )
270 242 recnd 
 |-  ( ch -> z e. CC )
271 269 270 abssubd 
 |-  ( ch -> ( abs ` ( B - z ) ) = ( abs ` ( z - B ) ) )
272 268 271 breqtrd 
 |-  ( ch -> ( B - z ) <_ ( abs ` ( z - B ) ) )
273 199 simprd 
 |-  ( ch -> ( abs ` ( z - B ) ) < ( 1 / j ) )
274 264 267 263 272 273 lelttrd 
 |-  ( ch -> ( B - z ) < ( 1 / j ) )
275 247 242 263 274 ltsub23d 
 |-  ( ch -> ( B - ( 1 / j ) ) < z )
276 201 35 syl 
 |-  ( ch -> A e. RR* )
277 iooltub 
 |-  ( ( A e. RR* /\ B e. RR* /\ z e. ( A (,) B ) ) -> z < B )
278 276 260 203 277 syl3anc 
 |-  ( ch -> z < B )
279 259 260 242 275 278 eliood 
 |-  ( ch -> z e. ( ( B - ( 1 / j ) ) (,) B ) )
280 246 247 202 248 241 257 258 279 dvbdfbdioolem1 
 |-  ( ch -> ( ( abs ` ( ( F ` z ) - ( F ` ( B - ( 1 / j ) ) ) ) ) <_ ( Y x. ( z - ( B - ( 1 / j ) ) ) ) /\ ( abs ` ( ( F ` z ) - ( F ` ( B - ( 1 / j ) ) ) ) ) <_ ( Y x. ( B - A ) ) ) )
281 280 simpld 
 |-  ( ch -> ( abs ` ( ( F ` z ) - ( F ` ( B - ( 1 / j ) ) ) ) ) <_ ( Y x. ( z - ( B - ( 1 / j ) ) ) ) )
282 201 216 64 syl2anc 
 |-  ( ch -> ( 1 / j ) e. RR )
283 241 282 remulcld 
 |-  ( ch -> ( Y x. ( 1 / j ) ) e. RR )
284 157 149 ffvelrnd 
 |-  ( ph -> ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) e. RR )
285 284 recnd 
 |-  ( ph -> ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) e. CC )
286 285 abscld 
 |-  ( ph -> ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) e. RR )
287 285 absge0d 
 |-  ( ph -> 0 <_ ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) )
288 2fveq3 
 |-  ( x = ( ( A + B ) / 2 ) -> ( abs ` ( ( RR _D F ) ` x ) ) = ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) )
289 7 eqcomi 
 |-  sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) = Y
290 289 a1i 
 |-  ( x = ( ( A + B ) / 2 ) -> sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) = Y )
291 288 290 breq12d 
 |-  ( x = ( ( A + B ) / 2 ) -> ( ( abs ` ( ( RR _D F ) ` x ) ) <_ sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) <-> ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) <_ Y ) )
292 291 rspcva 
 |-  ( ( ( ( A + B ) / 2 ) e. ( A (,) B ) /\ A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) ) -> ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) <_ Y )
293 149 249 292 syl2anc 
 |-  ( ph -> ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) <_ Y )
294 22 286 165 287 293 letrd 
 |-  ( ph -> 0 <_ Y )
295 201 294 syl 
 |-  ( ch -> 0 <_ Y )
296 282 recnd 
 |-  ( ch -> ( 1 / j ) e. CC )
297 sub31 
 |-  ( ( z e. CC /\ B e. CC /\ ( 1 / j ) e. CC ) -> ( z - ( B - ( 1 / j ) ) ) = ( ( 1 / j ) - ( B - z ) ) )
298 270 269 296 297 syl3anc 
 |-  ( ch -> ( z - ( B - ( 1 / j ) ) ) = ( ( 1 / j ) - ( B - z ) ) )
299 242 247 posdifd 
 |-  ( ch -> ( z < B <-> 0 < ( B - z ) ) )
300 278 299 mpbid 
 |-  ( ch -> 0 < ( B - z ) )
301 264 300 elrpd 
 |-  ( ch -> ( B - z ) e. RR+ )
302 282 301 ltsubrpd 
 |-  ( ch -> ( ( 1 / j ) - ( B - z ) ) < ( 1 / j ) )
303 298 302 eqbrtrd 
 |-  ( ch -> ( z - ( B - ( 1 / j ) ) ) < ( 1 / j ) )
304 244 282 303 ltled 
 |-  ( ch -> ( z - ( B - ( 1 / j ) ) ) <_ ( 1 / j ) )
305 244 282 241 295 304 lemul2ad 
 |-  ( ch -> ( Y x. ( z - ( B - ( 1 / j ) ) ) ) <_ ( Y x. ( 1 / j ) ) )
306 283 adantr 
 |-  ( ( ch /\ Y = 0 ) -> ( Y x. ( 1 / j ) ) e. RR )
307 236 adantr 
 |-  ( ( ch /\ Y = 0 ) -> ( x / 2 ) e. RR )
308 oveq1 
 |-  ( Y = 0 -> ( Y x. ( 1 / j ) ) = ( 0 x. ( 1 / j ) ) )
309 296 mul02d 
 |-  ( ch -> ( 0 x. ( 1 / j ) ) = 0 )
310 308 309 sylan9eqr 
 |-  ( ( ch /\ Y = 0 ) -> ( Y x. ( 1 / j ) ) = 0 )
311 208 rphalfcld 
 |-  ( ch -> ( x / 2 ) e. RR+ )
312 311 rpgt0d 
 |-  ( ch -> 0 < ( x / 2 ) )
313 312 adantr 
 |-  ( ( ch /\ Y = 0 ) -> 0 < ( x / 2 ) )
314 310 313 eqbrtrd 
 |-  ( ( ch /\ Y = 0 ) -> ( Y x. ( 1 / j ) ) < ( x / 2 ) )
315 306 307 314 ltled 
 |-  ( ( ch /\ Y = 0 ) -> ( Y x. ( 1 / j ) ) <_ ( x / 2 ) )
316 241 adantr 
 |-  ( ( ch /\ -. Y = 0 ) -> Y e. RR )
317 295 adantr 
 |-  ( ( ch /\ -. Y = 0 ) -> 0 <_ Y )
318 neqne 
 |-  ( -. Y = 0 -> Y =/= 0 )
319 318 adantl 
 |-  ( ( ch /\ -. Y = 0 ) -> Y =/= 0 )
320 316 317 319 ne0gt0d 
 |-  ( ( ch /\ -. Y = 0 ) -> 0 < Y )
321 283 adantr 
 |-  ( ( ch /\ 0 < Y ) -> ( Y x. ( 1 / j ) ) e. RR )
322 15 211 sselid 
 |-  ( ch -> N e. RR )
323 0red 
 |-  ( ch -> 0 e. RR )
324 201 208 145 syl2anc 
 |-  ( ch -> M e. RR )
325 201 72 syl 
 |-  ( ch -> 0 < M )
326 201 208 188 syl2anc 
 |-  ( ch -> M <_ N )
327 323 324 322 325 326 ltletrd 
 |-  ( ch -> 0 < N )
328 327 gt0ne0d 
 |-  ( ch -> N =/= 0 )
329 322 328 rereccld 
 |-  ( ch -> ( 1 / N ) e. RR )
330 241 329 remulcld 
 |-  ( ch -> ( Y x. ( 1 / N ) ) e. RR )
331 330 adantr 
 |-  ( ( ch /\ 0 < Y ) -> ( Y x. ( 1 / N ) ) e. RR )
332 236 adantr 
 |-  ( ( ch /\ 0 < Y ) -> ( x / 2 ) e. RR )
333 282 adantr 
 |-  ( ( ch /\ 0 < Y ) -> ( 1 / j ) e. RR )
334 329 adantr 
 |-  ( ( ch /\ 0 < Y ) -> ( 1 / N ) e. RR )
335 241 adantr 
 |-  ( ( ch /\ 0 < Y ) -> Y e. RR )
336 295 adantr 
 |-  ( ( ch /\ 0 < Y ) -> 0 <_ Y )
337 322 327 elrpd 
 |-  ( ch -> N e. RR+ )
338 201 216 101 syl2anc 
 |-  ( ch -> j e. RR+ )
339 1red 
 |-  ( ch -> 1 e. RR )
340 103 a1i 
 |-  ( ch -> 0 <_ 1 )
341 215 190 syl 
 |-  ( ch -> N <_ j )
342 337 338 339 340 341 lediv2ad 
 |-  ( ch -> ( 1 / j ) <_ ( 1 / N ) )
343 342 adantr 
 |-  ( ( ch /\ 0 < Y ) -> ( 1 / j ) <_ ( 1 / N ) )
344 333 334 335 336 343 lemul2ad 
 |-  ( ( ch /\ 0 < Y ) -> ( Y x. ( 1 / j ) ) <_ ( Y x. ( 1 / N ) ) )
345 234 recnd 
 |-  ( ch -> x e. CC )
346 2cnd 
 |-  ( ch -> 2 e. CC )
347 208 rpne0d 
 |-  ( ch -> x =/= 0 )
348 175 a1i 
 |-  ( ch -> 2 =/= 0 )
349 345 346 347 348 divne0d 
 |-  ( ch -> ( x / 2 ) =/= 0 )
350 241 236 349 redivcld 
 |-  ( ch -> ( Y / ( x / 2 ) ) e. RR )
351 350 adantr 
 |-  ( ( ch /\ 0 < Y ) -> ( Y / ( x / 2 ) ) e. RR )
352 simpr 
 |-  ( ( ch /\ 0 < Y ) -> 0 < Y )
353 312 adantr 
 |-  ( ( ch /\ 0 < Y ) -> 0 < ( x / 2 ) )
354 335 332 352 353 divgt0d 
 |-  ( ( ch /\ 0 < Y ) -> 0 < ( Y / ( x / 2 ) ) )
355 351 354 elrpd 
 |-  ( ( ch /\ 0 < Y ) -> ( Y / ( x / 2 ) ) e. RR+ )
356 355 rprecred 
 |-  ( ( ch /\ 0 < Y ) -> ( 1 / ( Y / ( x / 2 ) ) ) e. RR )
357 337 adantr 
 |-  ( ( ch /\ 0 < Y ) -> N e. RR+ )
358 1red 
 |-  ( ( ch /\ 0 < Y ) -> 1 e. RR )
359 103 a1i 
 |-  ( ( ch /\ 0 < Y ) -> 0 <_ 1 )
360 350 flcld 
 |-  ( ch -> ( |_ ` ( Y / ( x / 2 ) ) ) e. ZZ )
361 360 peano2zd 
 |-  ( ch -> ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) e. ZZ )
362 361 zred 
 |-  ( ch -> ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) e. RR )
363 201 143 syl 
 |-  ( ch -> M e. ZZ )
364 361 363 ifcld 
 |-  ( ch -> if ( M <_ ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , M ) e. ZZ )
365 11 364 eqeltrid 
 |-  ( ch -> N e. ZZ )
366 365 zred 
 |-  ( ch -> N e. RR )
367 flltp1 
 |-  ( ( Y / ( x / 2 ) ) e. RR -> ( Y / ( x / 2 ) ) < ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) )
368 350 367 syl 
 |-  ( ch -> ( Y / ( x / 2 ) ) < ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) )
369 201 67 syl 
 |-  ( ch -> M e. RR )
370 max2 
 |-  ( ( M e. RR /\ ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) e. RR ) -> ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) <_ if ( M <_ ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , M ) )
371 369 362 370 syl2anc 
 |-  ( ch -> ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) <_ if ( M <_ ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , M ) )
372 371 11 breqtrrdi 
 |-  ( ch -> ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) <_ N )
373 350 362 366 368 372 ltletrd 
 |-  ( ch -> ( Y / ( x / 2 ) ) < N )
374 350 322 373 ltled 
 |-  ( ch -> ( Y / ( x / 2 ) ) <_ N )
375 374 adantr 
 |-  ( ( ch /\ 0 < Y ) -> ( Y / ( x / 2 ) ) <_ N )
376 355 357 358 359 375 lediv2ad 
 |-  ( ( ch /\ 0 < Y ) -> ( 1 / N ) <_ ( 1 / ( Y / ( x / 2 ) ) ) )
377 334 356 335 336 376 lemul2ad 
 |-  ( ( ch /\ 0 < Y ) -> ( Y x. ( 1 / N ) ) <_ ( Y x. ( 1 / ( Y / ( x / 2 ) ) ) ) )
378 335 recnd 
 |-  ( ( ch /\ 0 < Y ) -> Y e. CC )
379 351 recnd 
 |-  ( ( ch /\ 0 < Y ) -> ( Y / ( x / 2 ) ) e. CC )
380 354 gt0ne0d 
 |-  ( ( ch /\ 0 < Y ) -> ( Y / ( x / 2 ) ) =/= 0 )
381 378 379 380 divrecd 
 |-  ( ( ch /\ 0 < Y ) -> ( Y / ( Y / ( x / 2 ) ) ) = ( Y x. ( 1 / ( Y / ( x / 2 ) ) ) ) )
382 332 recnd 
 |-  ( ( ch /\ 0 < Y ) -> ( x / 2 ) e. CC )
383 352 gt0ne0d 
 |-  ( ( ch /\ 0 < Y ) -> Y =/= 0 )
384 349 adantr 
 |-  ( ( ch /\ 0 < Y ) -> ( x / 2 ) =/= 0 )
385 378 382 383 384 ddcand 
 |-  ( ( ch /\ 0 < Y ) -> ( Y / ( Y / ( x / 2 ) ) ) = ( x / 2 ) )
386 381 385 eqtr3d 
 |-  ( ( ch /\ 0 < Y ) -> ( Y x. ( 1 / ( Y / ( x / 2 ) ) ) ) = ( x / 2 ) )
387 377 386 breqtrd 
 |-  ( ( ch /\ 0 < Y ) -> ( Y x. ( 1 / N ) ) <_ ( x / 2 ) )
388 321 331 332 344 387 letrd 
 |-  ( ( ch /\ 0 < Y ) -> ( Y x. ( 1 / j ) ) <_ ( x / 2 ) )
389 320 388 syldan 
 |-  ( ( ch /\ -. Y = 0 ) -> ( Y x. ( 1 / j ) ) <_ ( x / 2 ) )
390 315 389 pm2.61dan 
 |-  ( ch -> ( Y x. ( 1 / j ) ) <_ ( x / 2 ) )
391 245 283 236 305 390 letrd 
 |-  ( ch -> ( Y x. ( z - ( B - ( 1 / j ) ) ) ) <_ ( x / 2 ) )
392 240 245 236 281 391 letrd 
 |-  ( ch -> ( abs ` ( ( F ` z ) - ( F ` ( B - ( 1 / j ) ) ) ) ) <_ ( x / 2 ) )
393 239 392 eqbrtrd 
 |-  ( ch -> ( abs ` ( ( F ` z ) - ( S ` j ) ) ) <_ ( x / 2 ) )
394 simpllr 
 |-  ( ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( z - B ) ) < ( 1 / j ) ) -> ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) )
395 199 394 syl 
 |-  ( ch -> ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) )
396 230 232 236 236 393 395 leltaddd 
 |-  ( ch -> ( ( abs ` ( ( F ` z ) - ( S ` j ) ) ) + ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) ) < ( ( x / 2 ) + ( x / 2 ) ) )
397 345 2halvesd 
 |-  ( ch -> ( ( x / 2 ) + ( x / 2 ) ) = x )
398 396 397 breqtrd 
 |-  ( ch -> ( ( abs ` ( ( F ` z ) - ( S ` j ) ) ) + ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) ) < x )
399 228 233 234 235 398 lelttrd 
 |-  ( ch -> ( abs ` ( ( ( F ` z ) - ( S ` j ) ) + ( ( S ` j ) - ( limsup ` S ) ) ) ) < x )
400 222 399 eqbrtrd 
 |-  ( ch -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) < x )
401 12 400 sylbir 
 |-  ( ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( z - B ) ) < ( 1 / j ) ) -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) < x )
402 401 adantrl 
 |-  ( ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) /\ ( z =/= B /\ ( abs ` ( z - B ) ) < ( 1 / j ) ) ) -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) < x )
403 402 ex 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) -> ( ( z =/= B /\ ( abs ` ( z - B ) ) < ( 1 / j ) ) -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) < x ) )
404 403 ralrimiva 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) -> A. z e. ( A (,) B ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < ( 1 / j ) ) -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) < x ) )
405 brimralrspcev 
 |-  ( ( ( 1 / j ) e. RR+ /\ A. z e. ( A (,) B ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < ( 1 / j ) ) -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) < x ) ) -> E. y e. RR+ A. z e. ( A (,) B ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) < x ) )
406 198 404 405 syl2anc 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) -> E. y e. RR+ A. z e. ( A (,) B ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) < x ) )
407 simpr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ b <_ N ) -> b <_ N )
408 407 iftrued 
 |-  ( ( ( ph /\ x e. RR+ ) /\ b <_ N ) -> if ( b <_ N , N , b ) = N )
409 uzid 
 |-  ( N e. ZZ -> N e. ( ZZ>= ` N ) )
410 182 409 syl 
 |-  ( ( ph /\ x e. RR+ ) -> N e. ( ZZ>= ` N ) )
411 410 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ b <_ N ) -> N e. ( ZZ>= ` N ) )
412 408 411 eqeltrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ b <_ N ) -> if ( b <_ N , N , b ) e. ( ZZ>= ` N ) )
413 412 adantlr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ b <_ N ) -> if ( b <_ N , N , b ) e. ( ZZ>= ` N ) )
414 iffalse 
 |-  ( -. b <_ N -> if ( b <_ N , N , b ) = b )
415 414 adantl 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ -. b <_ N ) -> if ( b <_ N , N , b ) = b )
416 182 ad2antrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ -. b <_ N ) -> N e. ZZ )
417 simplr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ -. b <_ N ) -> b e. ZZ )
418 416 zred 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ -. b <_ N ) -> N e. RR )
419 417 zred 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ -. b <_ N ) -> b e. RR )
420 simpr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ -. b <_ N ) -> -. b <_ N )
421 418 419 ltnled 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ -. b <_ N ) -> ( N < b <-> -. b <_ N ) )
422 420 421 mpbird 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ -. b <_ N ) -> N < b )
423 418 419 422 ltled 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ -. b <_ N ) -> N <_ b )
424 eluz2 
 |-  ( b e. ( ZZ>= ` N ) <-> ( N e. ZZ /\ b e. ZZ /\ N <_ b ) )
425 416 417 423 424 syl3anbrc 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ -. b <_ N ) -> b e. ( ZZ>= ` N ) )
426 415 425 eqeltrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ -. b <_ N ) -> if ( b <_ N , N , b ) e. ( ZZ>= ` N ) )
427 413 426 pm2.61dan 
 |-  ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) -> if ( b <_ N , N , b ) e. ( ZZ>= ` N ) )
428 427 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) ) -> if ( b <_ N , N , b ) e. ( ZZ>= ` N ) )
429 simpr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) ) -> A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) )
430 simpr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) -> b e. ZZ )
431 182 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) -> N e. ZZ )
432 431 430 ifcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) -> if ( b <_ N , N , b ) e. ZZ )
433 430 zred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) -> b e. RR )
434 431 zred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) -> N e. RR )
435 max1 
 |-  ( ( b e. RR /\ N e. RR ) -> b <_ if ( b <_ N , N , b ) )
436 433 434 435 syl2anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) -> b <_ if ( b <_ N , N , b ) )
437 eluz2 
 |-  ( if ( b <_ N , N , b ) e. ( ZZ>= ` b ) <-> ( b e. ZZ /\ if ( b <_ N , N , b ) e. ZZ /\ b <_ if ( b <_ N , N , b ) ) )
438 430 432 436 437 syl3anbrc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) -> if ( b <_ N , N , b ) e. ( ZZ>= ` b ) )
439 438 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) ) -> if ( b <_ N , N , b ) e. ( ZZ>= ` b ) )
440 fveq2 
 |-  ( c = if ( b <_ N , N , b ) -> ( S ` c ) = ( S ` if ( b <_ N , N , b ) ) )
441 440 eleq1d 
 |-  ( c = if ( b <_ N , N , b ) -> ( ( S ` c ) e. CC <-> ( S ` if ( b <_ N , N , b ) ) e. CC ) )
442 440 fvoveq1d 
 |-  ( c = if ( b <_ N , N , b ) -> ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) = ( abs ` ( ( S ` if ( b <_ N , N , b ) ) - ( limsup ` S ) ) ) )
443 442 breq1d 
 |-  ( c = if ( b <_ N , N , b ) -> ( ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) <-> ( abs ` ( ( S ` if ( b <_ N , N , b ) ) - ( limsup ` S ) ) ) < ( x / 2 ) ) )
444 441 443 anbi12d 
 |-  ( c = if ( b <_ N , N , b ) -> ( ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) <-> ( ( S ` if ( b <_ N , N , b ) ) e. CC /\ ( abs ` ( ( S ` if ( b <_ N , N , b ) ) - ( limsup ` S ) ) ) < ( x / 2 ) ) ) )
445 444 rspccva 
 |-  ( ( A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ if ( b <_ N , N , b ) e. ( ZZ>= ` b ) ) -> ( ( S ` if ( b <_ N , N , b ) ) e. CC /\ ( abs ` ( ( S ` if ( b <_ N , N , b ) ) - ( limsup ` S ) ) ) < ( x / 2 ) ) )
446 429 439 445 syl2anc 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) ) -> ( ( S ` if ( b <_ N , N , b ) ) e. CC /\ ( abs ` ( ( S ` if ( b <_ N , N , b ) ) - ( limsup ` S ) ) ) < ( x / 2 ) ) )
447 446 simprd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) ) -> ( abs ` ( ( S ` if ( b <_ N , N , b ) ) - ( limsup ` S ) ) ) < ( x / 2 ) )
448 fveq2 
 |-  ( j = if ( b <_ N , N , b ) -> ( S ` j ) = ( S ` if ( b <_ N , N , b ) ) )
449 448 fvoveq1d 
 |-  ( j = if ( b <_ N , N , b ) -> ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) = ( abs ` ( ( S ` if ( b <_ N , N , b ) ) - ( limsup ` S ) ) ) )
450 449 breq1d 
 |-  ( j = if ( b <_ N , N , b ) -> ( ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) <-> ( abs ` ( ( S ` if ( b <_ N , N , b ) ) - ( limsup ` S ) ) ) < ( x / 2 ) ) )
451 450 rspcev 
 |-  ( ( if ( b <_ N , N , b ) e. ( ZZ>= ` N ) /\ ( abs ` ( ( S ` if ( b <_ N , N , b ) ) - ( limsup ` S ) ) ) < ( x / 2 ) ) -> E. j e. ( ZZ>= ` N ) ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) )
452 428 447 451 syl2anc 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) ) -> E. j e. ( ZZ>= ` N ) ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) )
453 ax-resscn 
 |-  RR C_ CC
454 453 a1i 
 |-  ( ph -> RR C_ CC )
455 4 454 fssd 
 |-  ( ph -> F : ( A (,) B ) --> CC )
456 dvcn 
 |-  ( ( ( RR C_ CC /\ F : ( A (,) B ) --> CC /\ ( A (,) B ) C_ RR ) /\ dom ( RR _D F ) = ( A (,) B ) ) -> F e. ( ( A (,) B ) -cn-> CC ) )
457 454 455 153 5 456 syl31anc 
 |-  ( ph -> F e. ( ( A (,) B ) -cn-> CC ) )
458 cncffvrn 
 |-  ( ( RR C_ CC /\ F e. ( ( A (,) B ) -cn-> CC ) ) -> ( F e. ( ( A (,) B ) -cn-> RR ) <-> F : ( A (,) B ) --> RR ) )
459 454 457 458 syl2anc 
 |-  ( ph -> ( F e. ( ( A (,) B ) -cn-> RR ) <-> F : ( A (,) B ) --> RR ) )
460 4 459 mpbird 
 |-  ( ph -> F e. ( ( A (,) B ) -cn-> RR ) )
461 110 10 fmptd 
 |-  ( ph -> R : ( ZZ>= ` M ) --> ( A (,) B ) )
462 eqid 
 |-  ( j e. ( ZZ>= ` M ) |-> ( F ` ( R ` j ) ) ) = ( j e. ( ZZ>= ` M ) |-> ( F ` ( R ` j ) ) )
463 climrel 
 |-  Rel ~~>
464 463 a1i 
 |-  ( ph -> Rel ~~> )
465 fvex 
 |-  ( ZZ>= ` M ) e. _V
466 465 mptex 
 |-  ( j e. ( ZZ>= ` M ) |-> B ) e. _V
467 466 a1i 
 |-  ( ph -> ( j e. ( ZZ>= ` M ) |-> B ) e. _V )
468 eqidd 
 |-  ( ( ph /\ m e. ( ZZ>= ` M ) ) -> ( j e. ( ZZ>= ` M ) |-> B ) = ( j e. ( ZZ>= ` M ) |-> B ) )
469 eqidd 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` M ) ) /\ j = m ) -> B = B )
470 simpr 
 |-  ( ( ph /\ m e. ( ZZ>= ` M ) ) -> m e. ( ZZ>= ` M ) )
471 2 adantr 
 |-  ( ( ph /\ m e. ( ZZ>= ` M ) ) -> B e. RR )
472 468 469 470 471 fvmptd 
 |-  ( ( ph /\ m e. ( ZZ>= ` M ) ) -> ( ( j e. ( ZZ>= ` M ) |-> B ) ` m ) = B )
473 31 30 467 92 472 climconst 
 |-  ( ph -> ( j e. ( ZZ>= ` M ) |-> B ) ~~> B )
474 465 mptex 
 |-  ( j e. ( ZZ>= ` M ) |-> ( B - ( 1 / j ) ) ) e. _V
475 10 474 eqeltri 
 |-  R e. _V
476 475 a1i 
 |-  ( ph -> R e. _V )
477 1cnd 
 |-  ( ph -> 1 e. CC )
478 elnnnn0b 
 |-  ( M e. NN <-> ( M e. NN0 /\ 0 < M ) )
479 29 72 478 sylanbrc 
 |-  ( ph -> M e. NN )
480 divcnvg 
 |-  ( ( 1 e. CC /\ M e. NN ) -> ( j e. ( ZZ>= ` M ) |-> ( 1 / j ) ) ~~> 0 )
481 477 479 480 syl2anc 
 |-  ( ph -> ( j e. ( ZZ>= ` M ) |-> ( 1 / j ) ) ~~> 0 )
482 eqidd 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( j e. ( ZZ>= ` M ) |-> B ) = ( j e. ( ZZ>= ` M ) |-> B ) )
483 eqidd 
 |-  ( ( ( ph /\ i e. ( ZZ>= ` M ) ) /\ j = i ) -> B = B )
484 simpr 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i e. ( ZZ>= ` M ) )
485 2 adantr 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> B e. RR )
486 482 483 484 485 fvmptd 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( ( j e. ( ZZ>= ` M ) |-> B ) ` i ) = B )
487 486 485 eqeltrd 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( ( j e. ( ZZ>= ` M ) |-> B ) ` i ) e. RR )
488 487 recnd 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( ( j e. ( ZZ>= ` M ) |-> B ) ` i ) e. CC )
489 eqidd 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( j e. ( ZZ>= ` M ) |-> ( 1 / j ) ) = ( j e. ( ZZ>= ` M ) |-> ( 1 / j ) ) )
490 oveq2 
 |-  ( j = i -> ( 1 / j ) = ( 1 / i ) )
491 490 adantl 
 |-  ( ( ( ph /\ i e. ( ZZ>= ` M ) ) /\ j = i ) -> ( 1 / j ) = ( 1 / i ) )
492 15 484 sselid 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i e. RR )
493 0red 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> 0 e. RR )
494 67 adantr 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> M e. RR )
495 72 adantr 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> 0 < M )
496 eluzle 
 |-  ( i e. ( ZZ>= ` M ) -> M <_ i )
497 496 adantl 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> M <_ i )
498 493 494 492 495 497 ltletrd 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> 0 < i )
499 498 gt0ne0d 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i =/= 0 )
500 492 499 rereccld 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( 1 / i ) e. RR )
501 489 491 484 500 fvmptd 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( ( j e. ( ZZ>= ` M ) |-> ( 1 / j ) ) ` i ) = ( 1 / i ) )
502 492 recnd 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i e. CC )
503 502 499 reccld 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( 1 / i ) e. CC )
504 501 503 eqeltrd 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( ( j e. ( ZZ>= ` M ) |-> ( 1 / j ) ) ` i ) e. CC )
505 490 oveq2d 
 |-  ( j = i -> ( B - ( 1 / j ) ) = ( B - ( 1 / i ) ) )
506 ovex 
 |-  ( B - ( 1 / i ) ) e. _V
507 505 10 506 fvmpt 
 |-  ( i e. ( ZZ>= ` M ) -> ( R ` i ) = ( B - ( 1 / i ) ) )
508 507 adantl 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( R ` i ) = ( B - ( 1 / i ) ) )
509 486 501 oveq12d 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( ( ( j e. ( ZZ>= ` M ) |-> B ) ` i ) - ( ( j e. ( ZZ>= ` M ) |-> ( 1 / j ) ) ` i ) ) = ( B - ( 1 / i ) ) )
510 508 509 eqtr4d 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( R ` i ) = ( ( ( j e. ( ZZ>= ` M ) |-> B ) ` i ) - ( ( j e. ( ZZ>= ` M ) |-> ( 1 / j ) ) ` i ) ) )
511 31 30 473 476 481 488 504 510 climsub 
 |-  ( ph -> R ~~> ( B - 0 ) )
512 92 subid1d 
 |-  ( ph -> ( B - 0 ) = B )
513 511 512 breqtrd 
 |-  ( ph -> R ~~> B )
514 releldm 
 |-  ( ( Rel ~~> /\ R ~~> B ) -> R e. dom ~~> )
515 464 513 514 syl2anc 
 |-  ( ph -> R e. dom ~~> )
516 fveq2 
 |-  ( l = k -> ( ZZ>= ` l ) = ( ZZ>= ` k ) )
517 fveq2 
 |-  ( l = k -> ( R ` l ) = ( R ` k ) )
518 517 oveq2d 
 |-  ( l = k -> ( ( R ` h ) - ( R ` l ) ) = ( ( R ` h ) - ( R ` k ) ) )
519 518 fveq2d 
 |-  ( l = k -> ( abs ` ( ( R ` h ) - ( R ` l ) ) ) = ( abs ` ( ( R ` h ) - ( R ` k ) ) ) )
520 519 breq1d 
 |-  ( l = k -> ( ( abs ` ( ( R ` h ) - ( R ` l ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) <-> ( abs ` ( ( R ` h ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) ) )
521 516 520 raleqbidv 
 |-  ( l = k -> ( A. h e. ( ZZ>= ` l ) ( abs ` ( ( R ` h ) - ( R ` l ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) <-> A. h e. ( ZZ>= ` k ) ( abs ` ( ( R ` h ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) ) )
522 521 cbvrabv 
 |-  { l e. ( ZZ>= ` M ) | A. h e. ( ZZ>= ` l ) ( abs ` ( ( R ` h ) - ( R ` l ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) } = { k e. ( ZZ>= ` M ) | A. h e. ( ZZ>= ` k ) ( abs ` ( ( R ` h ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) }
523 fveq2 
 |-  ( h = i -> ( R ` h ) = ( R ` i ) )
524 523 fvoveq1d 
 |-  ( h = i -> ( abs ` ( ( R ` h ) - ( R ` k ) ) ) = ( abs ` ( ( R ` i ) - ( R ` k ) ) ) )
525 524 breq1d 
 |-  ( h = i -> ( ( abs ` ( ( R ` h ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) <-> ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) ) )
526 525 cbvralvw 
 |-  ( A. h e. ( ZZ>= ` k ) ( abs ` ( ( R ` h ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) <-> A. i e. ( ZZ>= ` k ) ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) )
527 526 rgenw 
 |-  A. k e. ( ZZ>= ` M ) ( A. h e. ( ZZ>= ` k ) ( abs ` ( ( R ` h ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) <-> A. i e. ( ZZ>= ` k ) ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) )
528 rabbi 
 |-  ( A. k e. ( ZZ>= ` M ) ( A. h e. ( ZZ>= ` k ) ( abs ` ( ( R ` h ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) <-> A. i e. ( ZZ>= ` k ) ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) ) <-> { k e. ( ZZ>= ` M ) | A. h e. ( ZZ>= ` k ) ( abs ` ( ( R ` h ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) } = { k e. ( ZZ>= ` M ) | A. i e. ( ZZ>= ` k ) ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) } )
529 527 528 mpbi 
 |-  { k e. ( ZZ>= ` M ) | A. h e. ( ZZ>= ` k ) ( abs ` ( ( R ` h ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) } = { k e. ( ZZ>= ` M ) | A. i e. ( ZZ>= ` k ) ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) }
530 522 529 eqtri 
 |-  { l e. ( ZZ>= ` M ) | A. h e. ( ZZ>= ` l ) ( abs ` ( ( R ` h ) - ( R ` l ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) } = { k e. ( ZZ>= ` M ) | A. i e. ( ZZ>= ` k ) ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) }
531 530 infeq1i 
 |-  inf ( { l e. ( ZZ>= ` M ) | A. h e. ( ZZ>= ` l ) ( abs ` ( ( R ` h ) - ( R ` l ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) } , RR , < ) = inf ( { k e. ( ZZ>= ` M ) | A. i e. ( ZZ>= ` k ) ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) } , RR , < )
532 1 2 3 460 5 6 30 461 462 515 531 ioodvbdlimc1lem1 
 |-  ( ph -> ( j e. ( ZZ>= ` M ) |-> ( F ` ( R ` j ) ) ) ~~> ( limsup ` ( j e. ( ZZ>= ` M ) |-> ( F ` ( R ` j ) ) ) ) )
533 10 fvmpt2 
 |-  ( ( j e. ( ZZ>= ` M ) /\ ( B - ( 1 / j ) ) e. RR ) -> ( R ` j ) = ( B - ( 1 / j ) ) )
534 115 65 533 syl2anc 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( R ` j ) = ( B - ( 1 / j ) ) )
535 534 eqcomd 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( B - ( 1 / j ) ) = ( R ` j ) )
536 535 fveq2d 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( F ` ( B - ( 1 / j ) ) ) = ( F ` ( R ` j ) ) )
537 536 mpteq2dva 
 |-  ( ph -> ( j e. ( ZZ>= ` M ) |-> ( F ` ( B - ( 1 / j ) ) ) ) = ( j e. ( ZZ>= ` M ) |-> ( F ` ( R ` j ) ) ) )
538 9 537 syl5eq 
 |-  ( ph -> S = ( j e. ( ZZ>= ` M ) |-> ( F ` ( R ` j ) ) ) )
539 538 fveq2d 
 |-  ( ph -> ( limsup ` S ) = ( limsup ` ( j e. ( ZZ>= ` M ) |-> ( F ` ( R ` j ) ) ) ) )
540 532 538 539 3brtr4d 
 |-  ( ph -> S ~~> ( limsup ` S ) )
541 465 mptex 
 |-  ( j e. ( ZZ>= ` M ) |-> ( F ` ( B - ( 1 / j ) ) ) ) e. _V
542 9 541 eqeltri 
 |-  S e. _V
543 542 a1i 
 |-  ( ph -> S e. _V )
544 eqidd 
 |-  ( ( ph /\ c e. ZZ ) -> ( S ` c ) = ( S ` c ) )
545 543 544 clim 
 |-  ( ph -> ( S ~~> ( limsup ` S ) <-> ( ( limsup ` S ) e. CC /\ A. a e. RR+ E. b e. ZZ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < a ) ) ) )
546 540 545 mpbid 
 |-  ( ph -> ( ( limsup ` S ) e. CC /\ A. a e. RR+ E. b e. ZZ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < a ) ) )
547 546 simprd 
 |-  ( ph -> A. a e. RR+ E. b e. ZZ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < a ) )
548 547 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> A. a e. RR+ E. b e. ZZ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < a ) )
549 simpr 
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR+ )
550 549 rphalfcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( x / 2 ) e. RR+ )
551 breq2 
 |-  ( a = ( x / 2 ) -> ( ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < a <-> ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) )
552 551 anbi2d 
 |-  ( a = ( x / 2 ) -> ( ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < a ) <-> ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) ) )
553 552 rexralbidv 
 |-  ( a = ( x / 2 ) -> ( E. b e. ZZ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < a ) <-> E. b e. ZZ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) ) )
554 553 rspccva 
 |-  ( ( A. a e. RR+ E. b e. ZZ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < a ) /\ ( x / 2 ) e. RR+ ) -> E. b e. ZZ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) )
555 548 550 554 syl2anc 
 |-  ( ( ph /\ x e. RR+ ) -> E. b e. ZZ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) )
556 452 555 r19.29a 
 |-  ( ( ph /\ x e. RR+ ) -> E. j e. ( ZZ>= ` N ) ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) )
557 406 556 r19.29a 
 |-  ( ( ph /\ x e. RR+ ) -> E. y e. RR+ A. z e. ( A (,) B ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) < x ) )
558 557 ralrimiva 
 |-  ( ph -> A. x e. RR+ E. y e. RR+ A. z e. ( A (,) B ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) < x ) )
559 ioosscn 
 |-  ( A (,) B ) C_ CC
560 559 a1i 
 |-  ( ph -> ( A (,) B ) C_ CC )
561 455 560 92 ellimc3 
 |-  ( ph -> ( ( limsup ` S ) e. ( F limCC B ) <-> ( ( limsup ` S ) e. CC /\ A. x e. RR+ E. y e. RR+ A. z e. ( A (,) B ) ( ( z =/= B /\ ( abs ` ( z - B ) ) < y ) -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) < x ) ) ) )
562 138 558 561 mpbir2and 
 |-  ( ph -> ( limsup ` S ) e. ( F limCC B ) )